Commit 2025-02-11 15:35 6d9ce56c

View on Github →

chore(Algebra/Order): process porting notes (#21651)

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Modified Mathlib/Algebra/Order/CauSeq/Basic.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Algebra/Order/Group/Abs.lean

modified theorem abs_le

modified theorem le_abs'

Modified Mathlib/Algebra/Order/Group/Unbundled/Basic.lean

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

Modified Mathlib/Algebra/Order/Hom/Basic.lean

Modified Mathlib/Algebra/Order/Hom/Ring.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Algebra/Order/Interval/Set/Group.lean

Modified Mathlib/Algebra/Order/Kleene.lean

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/OrderDual.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

Modified Mathlib/Algebra/Order/Rearrangement.lean

Modified Mathlib/Algebra/Order/Ring/Abs.lean

Modified Mathlib/Algebra/Order/Ring/Prod.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

Modified Mathlib/Algebra/Order/Round.lean

Modified Mathlib/Algebra/Order/Star/Basic.lean

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

Modified Mathlib/Order/Interval/Finset/Box.lean