Commit 2025-04-10 16:38 c555785f

View on Github →

chore: deprecate semibundled ordered algebraic typeclasses (#20676) This PR deprecates 32 legacy semibundled Ordered* typeclasses and migrates to new mixin typeclasses IsOrdered(Cancel)(Add)Monoid and Is(Strict)OrderedRing. |Old|New| |

Estimated changes

added structure LinearOrderedField
added structure LinearOrderedSemifield
added structure LinearOrderedAddCommGroup
added structure LinearOrderedCommGroup
added structure OrderedAddCommGroup
added structure OrderedCommGroup
modified structure PositiveLinearMap
added structure LinearOrderedCommMonoid
added structure OrderedAddCommMonoid
added structure OrderedCancelCommMonoid
added structure OrderedCommMonoid
added theorem IsOrderedRing.mkOfCone
added structure LinearOrderedCommRing
added structure LinearOrderedCommSemiring
added structure LinearOrderedRing
added structure LinearOrderedSemiring
added structure OrderedCommRing
added structure OrderedCommSemiring
added structure OrderedRing
added structure OrderedSemiring
added structure StrictOrderedCommRing
added structure StrictOrderedCommSemiring
added structure StrictOrderedRing
added structure StrictOrderedSemiring
modified theorem IsNonarchimedean.add_le
modified theorem WithTop.untop₀_neg
modified theorem WithTop.untop₀_nonneg
modified def Subsemiring.nonneg
added structure NormedLinearOrderedField
added structure NormedLinearOrderedGroup
added structure NormedOrderedAddGroup
added structure NormedOrderedGroup
added structure NormedLatticeAddCommGroup
modified theorem Finsupp.degree_eq_zero_iff
modified theorem Finsupp.le_degree
modified theorem Num.cast_inj
modified theorem Num.cast_le
modified theorem Num.cast_lt
modified theorem PosNum.cast_le
modified theorem PosNum.cast_lt
modified theorem PosNum.cast_pos
modified theorem PosNum.one_le_cast
modified theorem ZNum.cast_inj
modified theorem ZNum.cast_le
modified theorem ZNum.cast_lt
modified theorem WithZero.mulArchimedean_iff
modified theorem Matrix.abs_det_reindex
modified theorem Filter.Germ.abs_def
modified theorem Filter.Germ.const_abs