Commit 2024-02-15 11:05 cbef07bb

View on Github →

feat(Topology.Algebra.Valuation): add integer_isOpen (#8148) The unit ball in a valued ring is open.

Estimated changes

Modified Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.mem_integer_iff

Modified Mathlib/Topology/Algebra/Valuation.lean

added theorem Valued.integer_isOpen

added theorem Valued.valuationSubring_isOpen