Theorem Valuation.Integers.dvdNotUnit_iff_lt

Modification history

2024-11-07 05:22

Mathlib/RingTheory/Valuation/Integers.lean

feat(RingTheory/Valuation/Integers): `dvdNotUnit_iff_lt` (#18482) …

Added Valuation.Integers.dvdNotUnit_iff_lt View on Github →