Theorem Valuation.Integers.valuation_pos_iff_ne_zero

Modification history

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