Commit 2024-03-28 17:08 d1a1aa1b

View on Github →

chore: move some aliases earlier (#11122)

Estimated changes

Modified Mathlib/Algebra/GroupPower/Order.lean

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

Modified Mathlib/Data/Tree.lean

Modified Mathlib/Init/Order/Defs.lean

added theorem le_rfl

Modified Mathlib/Order/Basic.lean

deleted theorem le_rfl