Commit 2023-10-31 09:38 1ff3bf34

View on Github →

chore: bump toolchain to v4.3.0-rc1 (#8051) This incorporates changes from

#7845
#7847
#7853
#7872 (was never actually made to work, but the diffs in nightly-testing are unexciting: we need to fully qualify a few names) They can all be closed when this is merged.

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/Algebra/Homology/Homology.lean

Modified Mathlib/Algebra/Homology/Single.lean

Modified Mathlib/Algebra/Jordan/Basic.lean

Modified Mathlib/Algebra/Order/CompleteField.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/Analysis/Analytic/Inverse.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/CategoryTheory/Comma.lean

modified theorem CategoryTheory.Comma.eqToHom_right

Modified Mathlib/CategoryTheory/DifferentialObject.lean

Modified Mathlib/CategoryTheory/Functor/Flat.lean

Modified Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

Modified Mathlib/Data/Complex/Module.lean

deleted theorem IsSelfAdjoint.imaginaryPart

Modified Mathlib/Data/Ordmap/Ordset.lean

Modified Mathlib/Data/Prod/TProd.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/UInt.lean

modified theorem UInt16.val_eq_of_lt

modified theorem UInt32.val_eq_of_lt

modified theorem UInt64.val_eq_of_lt

modified theorem UInt8.val_eq_of_lt

modified theorem USize.val_eq_of_lt

Modified Mathlib/Lean/Meta/DiscrTree.lean

modified def Lean.Meta.DiscrTree.insertIfSpecific

modified def Lean.Meta.DiscrTree.mapArrays

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

Modified Mathlib/Logic/Equiv/Set.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Measure/OuterMeasure.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/Probability/Kernel/Composition.lean

Modified Mathlib/Probability/Kernel/WithDensity.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/Tactic/Cache.lean

modified def Mathlib.Tactic.DiscrTreeCache.getMatch

Modified Mathlib/Tactic/LibrarySearch.lean

added def Mathlib.Tactic.LibrarySearch.discrTreeConfig

Modified Mathlib/Tactic/NormNum/Core.lean

added def Mathlib.Meta.NormNum.discrTreeConfig

Modified Mathlib/Tactic/Positivity/Core.lean

added def Mathlib.Meta.Positivity.discrTreeConfig

Modified Mathlib/Tactic/Propose.lean

added def Mathlib.Tactic.Propose.discrTreeConfig

modified def Mathlib.Tactic.Propose.propose

Modified Mathlib/Tactic/Relation/Rfl.lean

Modified Mathlib/Tactic/Relation/Trans.lean

added def Mathlib.Tactic.transExt.config

Modified Mathlib/Tactic/Rewrites.lean

added def Mathlib.Tactic.Rewrites.discrTreeConfig

Modified Mathlib/Tactic/Widget/Calc.lean

modified def createCalc

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/DenseEmbedding.lean

Modified lake-manifest.json

Modified lean-toolchain