Commit 2026-03-05 11:23 362209f2

View on Github →

feat(RingTheory/Valuation): add API (#36110) Prerequisites for #26872. Co-authored by: @faenuccio.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Range.lean

added theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff

added theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_range_eq_top

added theorem MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective

Modified Mathlib/Algebra/Order/GroupWithZero/Range.lean

added theorem MonoidWithZeroHom.ValueGroup₀.embedding_strictMono

added theorem MonoidWithZeroHom.ValueGroup₀.embedding_unit_ne_zero

added theorem MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos

deleted def MonoidWithZeroHom.ValueGroup₀.orderEmbedding

deleted theorem MonoidWithZeroHom.ValueGroup₀.orderEmbedding_apply

deleted theorem MonoidWithZeroHom.ValueGroup₀.orderEmbedding_mul

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.IsEquiv.restrict

added theorem Valuation.embedding_restrict

added theorem Valuation.exists_div_eq_of_unit

added def Valuation.restrict

added theorem Valuation.restrict_def

added theorem Valuation.restrict_eq_one_iff

added theorem Valuation.restrict_eq_zero_iff

added theorem Valuation.restrict_inj

added theorem Valuation.restrict_le_iff

added theorem Valuation.restrict_le_iff_le_embedding

added theorem Valuation.restrict_le_one_iff

added theorem Valuation.restrict_lt_iff

added theorem Valuation.restrict_lt_iff_lt_embedding

added theorem Valuation.restrict_lt_one_iff

added theorem Valuation.restrict_pos_iff