Commit 2024-04-30 16:16 e50e1c94

View on Github →

chore: adaptations to lean 4.8.0 (#12549)

Estimated changes

Modified Archive/Examples/IfNormalization/Result.lean

Modified Archive/Examples/IfNormalization/WithoutAesop.lean

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Archive/Wiedijk100Theorems/InverseTriangleSum.lean

Modified Mathlib/Algebra/BigOperators/Associated.lean

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Modified Mathlib/Algebra/Category/Ring/Limits.lean

Modified Mathlib/Algebra/Function/Support.lean

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Algebra/Group/UniqueProds.lean

Modified Mathlib/Algebra/Homology/Augment.lean

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

Modified Mathlib/Algebra/MvPolynomial/Polynomial.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Algebra/PUnitInstances.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Analysis/BoundedVariation.lean

Modified Mathlib/Analysis/Convex/Basic.lean

modified theorem stdSimplex_fin_two

Modified Mathlib/Analysis/NormedSpace/Star/Matrix.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

Modified Mathlib/Topology/UniformSpace/Matrix.lean

Modified docs/overview.yaml

Modified docs/undergrad.yaml