Commit 2024-05-01 16:10 bd932a42

View on Github →

chore: adaptations to lean 4.8.0 (#12578)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor.lean

Modified Mathlib/CategoryTheory/Category/Preorder.lean

modified theorem CategoryTheory.homOfLE_refl

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean

Modified Mathlib/Computability/Halting.lean

Modified Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

modified theorem List.Nat.antidiagonalTuple_zero_succ

Modified Mathlib/Data/List/GetD.lean

Modified Mathlib/Data/QPF/Univariate/Basic.lean

Modified Mathlib/Data/Rat/Defs.lean

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/Init/Data/Nat/Basic.lean

added theorem Nat.add_one_pos

Modified Mathlib/Init/Data/Nat/Lemmas.lean