Theorem ValuativeRel.ValueGroupWithZero.orderMonoidIso₀_embed

Modification history

2026-10-19 12:30
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat(RingTheory/Valuation/Discrete/IsDiscreteValuationSubring): equivalent discrete valuations (#43655) …
Added ValuativeRel.ValueGroupWithZero.orderMonoidIso₀_embedView on Github →