Theorem Valuation.Integers.valuation_irreducible_lt_one

Modification history

2025-07-06 22:36
Mathlib/RingTheory/Valuation/Integers.lean
chore(RingTheory/Valuation): generalize lemmas about valuation of irreducibles in subring (#26545) …
Added Valuation.Integers.valuation_irreducible_lt_oneView on Github →