Theorem IsValuativeTopology.of_isInducing

Modification history

2026-10-09 07:54
Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean
feat: `ValuativeRel` and `IsValuativeTopology (v.adicCompletion K)` (#44279) …
Added IsValuativeTopology.of_isInducingView on Github →