Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-10-02 11:20
f8412f2c
View on Github →
chore: deprecated modules for
#43253
(
#44401
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Bracket.lean
Created
Mathlib/Data/ENat/SuccOrder.lean
Created
Mathlib/Data/Fin/SuccPredOrder.lean
Created
Mathlib/Data/FunLike/Basic.lean
Created
Mathlib/Data/FunLike/Embedding.lean
Created
Mathlib/Data/FunLike/Equiv.lean
Created
Mathlib/Data/FunLike/Graded.lean
Created
Mathlib/Data/FunLike/Group.lean
Created
Mathlib/Data/FunLike/IsApply.lean
Created
Mathlib/Data/FunLike/Module.lean
Created
Mathlib/Data/FunLike/Ring.lean
Created
Mathlib/Data/Int/AbsoluteValue.lean
Created
Mathlib/Data/Int/ConditionallyCompleteOrder.lean
Created
Mathlib/Data/Int/LeastGreatest.lean
Created
Mathlib/Data/Int/Star.lean
Created
Mathlib/Data/Int/SuccPred.lean
Created
Mathlib/Data/Multiset/OrderedMonoid.lean
Created
Mathlib/Data/Nat/SuccPred.lean
Created
Mathlib/Data/Opposite.lean
Created
Mathlib/Data/PEquiv.lean
Created
Mathlib/Data/PNat/Order.lean
Created
Mathlib/Data/PSigma/Order.lean
Created
Mathlib/Data/Prod/Lex.lean
Created
Mathlib/Data/Rat/Star.lean
Created
Mathlib/Data/SProd.lean
Created
Mathlib/Data/Set/Pairwise/Chain.lean
Created
Mathlib/Data/SetLike/Basic.lean
Created
Mathlib/Data/Setoid/Basic.lean
Created
Mathlib/Data/Setoid/Partition.lean
Created
Mathlib/Data/Setoid/Partition/Card.lean
Created
Mathlib/Data/Sigma/Lex.lean
Created
Mathlib/Data/Sigma/Order.lean
Created
Mathlib/Data/Sum/Lattice.lean
Created
Mathlib/Data/Sum/Order.lean
Created
Mathlib/Data/Sym/Sym2/Order.lean