Theorem Valuation.Integers.isUnit_iff_valuation_eq_one

Modification history

2024-11-07 05:22
Mathlib/RingTheory/Valuation/Integers.lean
feat(RingTheory/Valuation/Integers): `dvdNotUnit_iff_lt` (#18482) …
Added Valuation.Integers.isUnit_iff_valuation_eq_oneView on Github →