Theorem Valuation.Integer.not_isUnit_iff_valuation_lt_one

Modification history

2025-04-14 15:20
Mathlib/RingTheory/Valuation/Integers.lean
feat(RingTheory/Valuation): add two lemmas about non-units in valuation subrings (#23408) …
Added Valuation.Integer.not_isUnit_iff_valuation_lt_oneView on Github →