Commit 2024-08-19 11:42 50a1bf0c

View on Github →

chore: backports from byAsSorry (#15759) A few backports to master from the byAsSorry branch.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

modified def AlgHom.equalizer

Modified Mathlib/Algebra/BigOperators/Group/List.lean

Modified Mathlib/Algebra/DirectLimit.lean

modified def Module.DirectLimit.lift

modified def Ring.DirectLimit.lift

Modified Mathlib/Algebra/Group/Subsemigroup/Operations.lean

modified def Subsemigroup.gciMapComap

Modified Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean

Modified Mathlib/Algebra/Homology/HomologySequence.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean

modified theorem CochainComplex.mappingCone.map_comp

Modified Mathlib/Algebra/Homology/HomotopyCofiber.lean

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

modified def Module.AEval.mapSubmodule

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

Modified Mathlib/Analysis/Analytic/IsolatedZeros.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/Convex/Caratheodory.lean

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/Data/Finset/Sort.lean

Modified Mathlib/Data/List/GetD.lean

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

Modified Mathlib/GroupTheory/PGroup.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

Modified Mathlib/MeasureTheory/Constructions/EventuallyMeasurable.lean

modified def EventuallyMeasurableSet

modified def EventuallyMeasurableSpace

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

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

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/AEDisjoint.lean

Modified Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean

Modified Mathlib/ModelTheory/DirectLimit.lean

modified def FirstOrder.Language.DirectLimit.lift

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/PellMatiyasevic.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/RingTheory/Derivation/Basic.lean

Modified Mathlib/RingTheory/Derivation/ToSquareZero.lean

modified def derivationToSquareZeroOfLift

modified def liftOfDerivationToSquareZero

Modified Mathlib/RingTheory/Int/Basic.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/Localization/NumDen.lean

Modified Mathlib/SetTheory/Ordinal/Topology.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

modified def Profinite.NobelingProof.GoodProducts.sum_equiv

modified def Profinite.NobelingProof.spanCone

modified def Profinite.NobelingProof.spanCone_isLimit

modified def Profinite.NobelingProof.spanFunctor

Modified Mathlib/Topology/Category/Profinite/Product.lean

modified def Profinite.indexCone

modified def Profinite.indexFunctor

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean

modified def TopCat.Presheaf.generateEquivalenceOpensLe

modified def TopCat.Presheaf.generateEquivalenceOpensLe_functor'

modified def TopCat.Presheaf.generateEquivalenceOpensLe_inverse'

modified def TopCat.Presheaf.isLimitOpensLeEquivGenerate₁

modified def TopCat.Presheaf.whiskerIsoMapGenerateCocone

Modified Mathlib/Topology/UnitInterval.lean