Theorem Valuation.integer.v_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.integer.v_irreducible_lt_oneView on Github →