Commit 2024-04-30 22:42 fd725829

View on Github →

chore: adaptations to lean 4.8.0 (#12562)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/CategoryTheory/Countable.lean

Modified Mathlib/CategoryTheory/Galois/Examples.lean

Modified Mathlib/CategoryTheory/Idempotents/Biproducts.lean

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

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/Combinatorics/Additive/Energy.lean

Modified Mathlib/Combinatorics/Derangements/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Data/Fin/VecNotation.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/List/ReduceOption.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/List/Sort.lean

added theorem List.length_split_fst_le

added theorem List.length_split_snd_le

Modified Mathlib/Data/List/Zip.lean

Modified Mathlib/Data/Multiset/FinsetOps.lean

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/Defs.lean

Modified Mathlib/Data/Nat/Digits.lean

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

Modified Mathlib/Data/Nat/Factors.lean

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Rat/Denumerable.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/FieldTheory/ChevalleyWarning.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Option.lean

Modified Mathlib/GroupTheory/GroupAction/Sigma.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Group/Convolution.lean

Modified docs/100.yaml