Theorem Valued.integer_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.integer_isOpenView on Github →
2025-04-02 23:37
Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
feat(Topology/Algebra/Valued/LocallyCompact): locally compact nonarchimedean field iff complete and DVR and finite field (#16733)
Modified Valued.integer_isOpenView on Github →
2024-02-15 11:05
Mathlib/Topology/Algebra/Valuation.lean
feat(Topology.Algebra.Valuation): add integer_isOpen (#8148) …
Added Valued.integer_isOpenView on Github →