Theorem Valuation.Integers.valuation_irreducible_pos

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_posView on Github →