Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-25 19:30
1dcc7221
View on Github →
chore(Order): remove unnecessary tactic invocations (
#28746
)
Estimated changes
Modified
Mathlib/Order/Basic.lean
modified
theorem
compl_ge
modified
theorem
compl_gt
modified
theorem
compl_le
modified
theorem
compl_lt
Modified
Mathlib/Order/CompleteLattice/Basic.lean
Modified
Mathlib/Order/Hom/Basic.lean
Modified
Mathlib/Order/Iterate.lean
Modified
Mathlib/Order/KonigLemma.lean
Modified
Mathlib/Order/PartialSups.lean
Modified
Mathlib/Order/Preorder/Chain.lean