Commit 2024-11-07 05:22 7c150141

View on Github →

feat(RingTheory/Valuation/Integers): dvdNotUnit_iff_lt (#18482) And isPrincipal_iff_exists_eq_setOf_valuation_le in preparation for showing WfDvdMonoid

Estimated changes

Modified Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.Integers.dvdNotUnit_iff_lt

added theorem Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le

added theorem Valuation.Integers.isUnit_iff_valuation_eq_one

added theorem Valuation.Integers.valuation_pos_iff_ne_zero