Commit 2025-11-19 06:07 6a54a808

View on Github →

chore: move Mathlib to the module system (#31786) This PR is a continuation of https://github.com/leanprover-community/mathlib4-nightly-testing/pull/80, but now targeting Mathlib master rather than nightly-testing.

Estimated changes

deleted def abs.unexpander
deleted def mabs.unexpander
deleted def WithLp.delabToLp
deleted def FinVec.mkProdEqQ
deleted def FinVec.mkSumEqQ
deleted def PiFin.mkLiteralQ
deleted def Finsupp.fun₀
deleted def precheckFinsetStx
modified theorem Nat.findGreatest_zero
modified theorem Nat.log2_two
deleted def Rat.evalIntCeil
deleted def Rat.evalIntFloor
deleted def Rat.evalIntFract
deleted def Rat.evalRound
modified theorem Stream'.Seq.length_nil
deleted def Vector3.unexpandNil
deleted def elabDeprecatedCross
deleted def Matrix.mkLiteralQ
deleted def mfld_cfg
deleted def Set.iUnion_delab
deleted def Set.sInter_delab
deleted def iInf_delab
deleted def iSup_delab
deleted def delabDeriv
modified theorem Mathlib.Tactic.Abel.term_eq
modified def LibraryNote
modified def Simps.findArgType