Theorem IsDiscreteValuationRing.exists_units_eq_smul_zpow_of_irreducible

Modification history

2026-04-14 10:54
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
feat(RingTheory): Order of vanishing in a discrete valuation ring (#29550) …
Added IsDiscreteValuationRing.exists_units_eq_smul_zpow_of_irreducibleView on Github →