Commit 2025-08-08 12:40 a8d2931a

View on Github →

chore: rename valuation_posSubmonoid_ne_zero_of_compatible (#28040) and sneak one more lemma in

Estimated changes

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

added theorem Valuation.apply_posSubmonoid_ne_zero

added theorem Valuation.apply_posSubmonoid_pos

deleted theorem ValuativeRel.valuation_posSubmonoid_ne_zero_of_compatible