Theorem Valued.valuationSubring_isOpen

Modification history

2025-05-04 06:34
Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
feat(Topology/Algebra/Valued): Add `IsClosed` and `IsClopen` lemmas (#24353) …
Deleted Valued.valuationSubring_isOpenView on Github →
2024-02-15 11:05
Mathlib/Topology/Algebra/Valuation.lean
feat(Topology.Algebra.Valuation): add integer_isOpen (#8148) …
Added Valued.valuationSubring_isOpenView on Github →