Theorem ValuativeRel.valuation_posSubmonoid_ne_zero_of_compatible

Modification history

2025-08-08 12:40
Mathlib/RingTheory/Valuation/ValuativeRel.lean
chore: rename valuation_posSubmonoid_ne_zero_of_compatible (#28040) …
Deleted ValuativeRel.valuation_posSubmonoid_ne_zero_of_compatibleView on Github →
2025-07-31 23:29
Mathlib/RingTheory/Valuation/ValuativeRel.lean
feat(RingTheory/ValuativeRel): IsRankLeOne when there is a compatible Zm0 or NNReal valuation (#27183) …
Added ValuativeRel.valuation_posSubmonoid_ne_zero_of_compatibleView on Github →