Theorem Valuation.Integers.valuation_unit

Modification history

2024-12-20 12:02
Mathlib/RingTheory/Valuation/Integers.lean
feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` (#15424)
Added Valuation.Integers.valuation_unitView on Github →