Theorem Valuation.mem_maximalIdeal_iff

Modification history

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