Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-02-24 10:38
0c08ce96
View on Github →
chore: bump toolchain to v4.29.0-rc2 (
#35708
)
Estimated changes
Modified
Archive/Imo/Imo1961Q3.lean
Modified
Archive/Imo/Imo1972Q5.lean
Modified
Archive/Imo/Imo1982Q1.lean
Modified
Archive/Imo/Imo1988Q6.lean
Modified
Archive/Imo/Imo1998Q2.lean
Modified
Archive/Imo/Imo2001Q4.lean
Modified
Archive/Imo/Imo2010Q5.lean
Modified
Archive/Imo/Imo2011Q3.lean
Modified
Archive/Imo/Imo2013Q5.lean
Modified
Archive/Imo/Imo2015Q6.lean
Modified
Archive/Imo/Imo2024Q1.lean
Modified
Archive/Imo/Imo2024Q3.lean
Modified
Archive/Imo/Imo2024Q6.lean
Modified
Archive/MiuLanguage/DecisionNec.lean
Modified
Archive/MiuLanguage/DecisionSuf.lean
Modified
Archive/Sensitivity.lean
Modified
Archive/Wiedijk100Theorems/AreaOfACircle.lean
Modified
Archive/Wiedijk100Theorems/BuffonsNeedle.lean
Modified
Archive/Wiedijk100Theorems/CubingACube.lean
Modified
Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean
Modified
Archive/ZagierTwoSquares.lean
Modified
Counterexamples/CliffordAlgebraNotInjective.lean
Modified
Counterexamples/DimensionPolynomial.lean
Modified
Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean
Modified
Counterexamples/NowhereDifferentiable.lean
Modified
Counterexamples/SeminormLatticeNotDistrib.lean
Modified
Counterexamples/SorgenfreyLine.lean
Modified
Counterexamples/TopologistsSineCurve.lean
Modified
Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean
Modified
Mathlib/Algebra/AddConstMap/Basic.lean
Modified
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Algebra/Operations.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
Modified
Mathlib/Algebra/BigOperators/Field.lean
Modified
Mathlib/Algebra/BigOperators/Fin.lean
Modified
Mathlib/Algebra/BigOperators/Intervals.lean
Modified
Mathlib/Algebra/BigOperators/ModEq.lean
Modified
Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
Modified
Mathlib/Algebra/Category/CommBialgCat.lean
Modified
Mathlib/Algebra/Category/Grp/EnoughInjectives.lean
Modified
Mathlib/Algebra/Category/Grp/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/Grp/FiniteGrp.lean
Modified
Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
Modified
Mathlib/Algebra/Category/Ring/Adjunctions.lean
Modified
Mathlib/Algebra/Central/End.lean
Modified
Mathlib/Algebra/CharP/Defs.lean
Modified
Mathlib/Algebra/CharP/Invertible.lean
Modified
Mathlib/Algebra/CharP/Lemmas.lean
Modified
Mathlib/Algebra/CharP/LinearMaps.lean
Modified
Mathlib/Algebra/DirectSum/Internal.lean
Modified
Mathlib/Algebra/Field/Periodic.lean
Modified
Mathlib/Algebra/Field/Subfield/Defs.lean
Modified
Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean
Modified
Mathlib/Algebra/FreeAlgebra.lean
Modified
Mathlib/Algebra/GCDMonoid/Basic.lean
Modified
Mathlib/Algebra/Group/Action/Hom.lean
Modified
Mathlib/Algebra/Group/Defs.lean
Modified
Mathlib/Algebra/Group/Fin/Basic.lean
Modified
Mathlib/Algebra/Group/ForwardDiff.lean
Modified
Mathlib/Algebra/Group/NatPowAssoc.lean
Modified
Mathlib/Algebra/Group/Subgroup/Ker.lean
Modified
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
Modified
Mathlib/Algebra/Homology/Functor.lean
Modified
Mathlib/Algebra/Homology/Homotopy.lean
Modified
Mathlib/Algebra/Jordan/Basic.lean
Modified
Mathlib/Algebra/Lie/Derivation/Basic.lean
Modified
Mathlib/Algebra/Lie/Engel.lean
Modified
Mathlib/Algebra/Lie/EngelSubalgebra.lean
Modified
Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean
Modified
Mathlib/Algebra/Lie/OfAssociative.lean
Modified
Mathlib/Algebra/Lie/Quotient.lean
Modified
Mathlib/Algebra/Lie/Sl2.lean
Modified
Mathlib/Algebra/Lie/Solvable.lean
Modified
Mathlib/Algebra/Lie/Subalgebra.lean
Modified
Mathlib/Algebra/Lie/Submodule.lean
Modified
Mathlib/Algebra/Lie/TraceForm.lean
Modified
Mathlib/Algebra/Lie/Weights/Basic.lean
Modified
Mathlib/Algebra/Lie/Weights/Cartan.lean
Modified
Mathlib/Algebra/Lie/Weights/Chain.lean
Modified
Mathlib/Algebra/Lie/Weights/IsSimple.lean
Modified
Mathlib/Algebra/Lie/Weights/Killing.lean
Modified
Mathlib/Algebra/Lie/Weights/Linear.lean
Modified
Mathlib/Algebra/Lie/Weights/RootSystem.lean
Modified
Mathlib/Algebra/Module/CharacterModule.lean
Modified
Mathlib/Algebra/Module/DedekindDomain.lean
Modified
Mathlib/Algebra/Module/FinitePresentation.lean
Modified
Mathlib/Algebra/Module/Injective.lean
Modified
Mathlib/Algebra/Module/NatInt.lean
Modified
Mathlib/Algebra/Module/PID.lean
Modified
Mathlib/Algebra/Module/Submodule/Pointwise.lean
Modified
Mathlib/Algebra/Module/ZLattice/Covolume.lean
Modified
Mathlib/Algebra/MvPolynomial/Degrees.lean
Modified
Mathlib/Algebra/Order/CauSeq/BigOperators.lean
Modified
Mathlib/Algebra/Order/Floor/Ring.lean
Modified
Mathlib/Algebra/Order/Floor/Semiring.lean
Modified
Mathlib/Algebra/Order/Group/Finset.lean
Modified
Mathlib/Algebra/Order/Module/Basic.lean
Modified
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
Modified
Mathlib/Algebra/Order/Nonneg/Lattice.lean
Modified
Mathlib/Algebra/Order/Nonneg/Ring.lean
Modified
Mathlib/Algebra/Order/Ring/Idempotent.lean
Modified
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
Modified
Mathlib/Algebra/Order/Ring/Nat.lean
Modified
Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
Modified
Mathlib/Algebra/Order/ToIntervalMod.lean
Modified
Mathlib/Algebra/Polynomial/Degree/Operations.lean
Modified
Mathlib/Algebra/Polynomial/Derivative.lean
Modified
Mathlib/Algebra/Polynomial/Expand.lean
Modified
Mathlib/Algebra/Polynomial/FieldDivision.lean
Modified
Mathlib/Algebra/Polynomial/HasseDeriv.lean
Modified
Mathlib/Algebra/Polynomial/Laurent.lean
Modified
Mathlib/Algebra/Polynomial/Mirror.lean
Modified
Mathlib/Algebra/Polynomial/Module/AEval.lean
deleted
def
Module.AEval.mapSubmodule
Modified
Mathlib/Algebra/Polynomial/Monic.lean
Modified
Mathlib/Algebra/Polynomial/OfFn.lean
deleted
def
Polynomial.toFn
Modified
Mathlib/Algebra/Polynomial/Roots.lean
Modified
Mathlib/Algebra/Polynomial/Smeval.lean
Modified
Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
Modified
Mathlib/Algebra/Polynomial/UnitTrinomial.lean
Modified
Mathlib/Algebra/Quandle.lean
Modified
Mathlib/Algebra/Quaternion.lean
Modified
Mathlib/Algebra/Ring/GeomSum.lean
Modified
Mathlib/Algebra/Ring/Int/Parity.lean
Modified
Mathlib/Algebra/Ring/Invertible.lean
Modified
Mathlib/Algebra/Ring/Periodic.lean
Modified
Mathlib/Algebra/Ring/Prod.lean
Modified
Mathlib/Algebra/Ring/Subring/Basic.lean
Modified
Mathlib/Algebra/RingQuot.lean
Modified
Mathlib/Algebra/Star/LinearMap.lean
Modified
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Symmetrized.lean
Modified
Mathlib/Algebra/TrivSqZeroExt.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
Modified
Mathlib/AlgebraicGeometry/Normalization.lean
Modified
Mathlib/AlgebraicGeometry/PointsPi.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
Modified
Mathlib/AlgebraicGeometry/Pullbacks.lean
Modified
Mathlib/AlgebraicGeometry/Scheme.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean
Modified
Mathlib/Analysis/Analytic/Order.lean
Modified
Mathlib/Analysis/Asymptotics/Lemmas.lean
Modified
Mathlib/Analysis/BoundedVariation.lean
Modified
Mathlib/Analysis/BoxIntegral/Basic.lean
Modified
Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
Modified
Mathlib/Analysis/BoxIntegral/UnitPartition.lean
Modified
Mathlib/Analysis/CStarAlgebra/Basic.lean
Modified
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/Classes.lean
Modified
Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
Modified
Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.lean
Modified
Mathlib/Analysis/CStarAlgebra/Hom.lean
Modified
Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
Modified
Mathlib/Analysis/CStarAlgebra/Projection.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/InnerProduct.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Defs.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean
Modified
Mathlib/Analysis/Calculus/Deriv/ZPow.lean
Modified
Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Norm.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
Modified
Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean
Modified
Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
Modified
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
Modified
Mathlib/Analysis/Calculus/Monotone.lean
Modified
Mathlib/Analysis/Complex/AbelLimit.lean
Modified
Mathlib/Analysis/Complex/Convex.lean
Modified
Mathlib/Analysis/Complex/CoveringMap.lean
Modified
Mathlib/Analysis/Complex/MeanValue.lean
Modified
Mathlib/Analysis/Complex/Periodic.lean
Modified
Mathlib/Analysis/Complex/Tietze.lean
Modified
Mathlib/Analysis/Complex/UnitDisc/Basic.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
Modified
Mathlib/Analysis/Convex/Birkhoff.lean
Modified
Mathlib/Analysis/Convex/Cone/InnerDual.lean
deleted
def
ProperCone.innerDual
Modified
Mathlib/Analysis/Convex/Continuous.lean
Modified
Mathlib/Analysis/Convex/Contractible.lean
Modified
Mathlib/Analysis/Convex/Deriv.lean
Modified
Mathlib/Analysis/Convex/Gauge.lean
Modified
Mathlib/Analysis/Convex/Intrinsic.lean
Modified
Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
Modified
Mathlib/Analysis/Convex/StrictConvexBetween.lean
Modified
Mathlib/Analysis/Convex/StrictConvexSpace.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean
Modified
Mathlib/Analysis/Distribution/TestFunction.lean
Modified
Mathlib/Analysis/Fourier/AddCircle.lean
Modified
Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
Modified
Mathlib/Analysis/Fourier/FourierTransform.lean
Modified
Mathlib/Analysis/Fourier/LpSpace.lean
Modified
Mathlib/Analysis/Fourier/PoissonSummation.lean
Modified
Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
Modified
Mathlib/Analysis/Fourier/ZMod.lean
Modified
Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
Modified
Mathlib/Analysis/Hofer.lean
Modified
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Calculus.lean
Modified
Mathlib/Analysis/InnerProductSpace/Coalgebra.lean
Modified
Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean
Modified
Mathlib/Analysis/InnerProductSpace/LinearMap.lean
Modified
Mathlib/Analysis/InnerProductSpace/Orientation.lean
Modified
Mathlib/Analysis/InnerProductSpace/PiL2.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Minimal.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean
Modified
Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
Modified
Mathlib/Analysis/InnerProductSpace/Spectrum.lean
Modified
Mathlib/Analysis/InnerProductSpace/TwoDim.lean
Modified
Mathlib/Analysis/InnerProductSpace/l2Space.lean
Modified
Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
Modified
Mathlib/Analysis/LocallyConvex/SeparatingDual.lean
Modified
Mathlib/Analysis/LocallyConvex/WeakDual.lean
Modified
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
Modified
Mathlib/Analysis/Matrix/Order.lean
Modified
Mathlib/Analysis/MellinInversion.lean
Modified
Mathlib/Analysis/MellinTransform.lean
Modified
Mathlib/Analysis/Normed/Affine/AddTorsor.lean
Modified
Mathlib/Analysis/Normed/Algebra/Exponential.lean
Modified
Mathlib/Analysis/Normed/Algebra/Unitization.lean
Modified
Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean
Modified
Mathlib/Analysis/Normed/Field/Lemmas.lean
Modified
Mathlib/Analysis/Normed/Field/Ultra.lean
Modified
Mathlib/Analysis/Normed/Group/AddCircle.lean
Modified
Mathlib/Analysis/Normed/Group/Basic.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
deleted
def
SemiNormedGrp.fork
Modified
Mathlib/Analysis/Normed/Lp/PiLp.lean
Modified
Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/Action.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/Homeomorph.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/RadialEquiv.lean
Modified
Mathlib/Analysis/Normed/Module/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/Connected.lean
Modified
Mathlib/Analysis/Normed/Module/Convex.lean
Modified
Mathlib/Analysis/Normed/Module/FiniteDimension.lean
Modified
Mathlib/Analysis/Normed/Module/HahnBanach.lean
Modified
Mathlib/Analysis/Normed/Module/MStructure.lean
Modified
Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean
Modified
Mathlib/Analysis/Normed/Module/RCLike/Extend.lean
Modified
Mathlib/Analysis/Normed/Module/RCLike/Real.lean
Modified
Mathlib/Analysis/Normed/Operator/Banach.lean
Modified
Mathlib/Analysis/Normed/Operator/Basic.lean
Modified
Mathlib/Analysis/Normed/Operator/Mul.lean
Modified
Mathlib/Analysis/Normed/Operator/NormedSpace.lean
Modified
Mathlib/Analysis/Normed/Operator/Prod.lean
Modified
Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
Modified
Mathlib/Analysis/Normed/Unbundled/IsPowMulFaithful.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
Modified
Mathlib/Analysis/Oscillation.lean
Modified
Mathlib/Analysis/PSeries.lean
Modified
Mathlib/Analysis/Polynomial/Fourier.lean
Modified
Mathlib/Analysis/Polynomial/MahlerMeasure.lean
Modified
Mathlib/Analysis/RCLike/Basic.lean
Modified
Mathlib/Analysis/RCLike/Sqrt.lean
Modified
Mathlib/Analysis/RCLike/TangentCone.lean
Modified
Mathlib/Analysis/Real/Cardinality.lean
Modified
Mathlib/Analysis/Real/Hyperreal.lean
Modified
Mathlib/Analysis/Real/OfDigits.lean
Modified
Mathlib/Analysis/Real/Pi/Irrational.lean
Modified
Mathlib/Analysis/Seminorm.lean
Modified
Mathlib/Analysis/SpecialFunctions/Bernstein.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
Modified
Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
Modified
Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
Modified
Mathlib/Analysis/SpecialFunctions/Sigmoid.lean
Modified
Mathlib/Analysis/SpecialFunctions/Stirling.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
Modified
Mathlib/Analysis/SpecificLimits/Fibonacci.lean
Modified
Mathlib/Analysis/SpecificLimits/Normed.lean
Modified
Mathlib/CategoryTheory/Action.lean
Modified
Mathlib/CategoryTheory/Action/Monoidal.lean
Modified
Mathlib/CategoryTheory/Adjunction/Basic.lean
Modified
Mathlib/CategoryTheory/Bicategory/Coherence.lean
Modified
Mathlib/CategoryTheory/Bicategory/SingleObj.lean
Modified
Mathlib/CategoryTheory/Enriched/Opposite.lean
Modified
Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
Modified
Mathlib/CategoryTheory/Groupoid.lean
Modified
Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
Modified
Mathlib/CategoryTheory/Limits/Bicones.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Modified
Mathlib/CategoryTheory/Localization/HomEquiv.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/ExponentiableMorphism.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Comon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
Modified
Mathlib/CategoryTheory/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Grp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Opposite/Mon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Transport.lean
Modified
Mathlib/CategoryTheory/Preadditive/Mat.lean
Modified
Mathlib/CategoryTheory/Shift/Basic.lean
Modified
Mathlib/CategoryTheory/Shift/Localization.lean
Modified
Mathlib/CategoryTheory/SingleObj.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean
Modified
Mathlib/CategoryTheory/Sites/Descent/DescentData.lean
Modified
Mathlib/CategoryTheory/Sites/Descent/DescentDataAsCoalgebra.lean
Modified
Mathlib/CategoryTheory/Sites/Sheafification.lean
Modified
Mathlib/CategoryTheory/Subfunctor/Equalizer.lean
Modified
Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
Modified
Mathlib/Combinatorics/Additive/Corner/Roth.lean
Modified
Mathlib/Combinatorics/Additive/ETransform.lean
Modified
Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
Modified
Mathlib/Combinatorics/Additive/RuzsaCovering.lean
Modified
Mathlib/Combinatorics/Additive/SmallTripling.lean
Modified
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
Modified
Mathlib/Combinatorics/Configuration.lean
Modified
Mathlib/Combinatorics/Enumerative/Bell.lean
Modified
Mathlib/Combinatorics/Enumerative/Catalan.lean
Modified
Mathlib/Combinatorics/Enumerative/DyckWord.lean
Modified
Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean
deleted
def
Nat.Partition.genFun
Modified
Mathlib/Combinatorics/Enumerative/Schroder.lean
Modified
Mathlib/Combinatorics/Nullstellensatz.lean
Modified
Mathlib/Combinatorics/Quiver/Symmetric.lean
Modified
Mathlib/Combinatorics/Schnirelmann.lean
Modified
Mathlib/Combinatorics/SetFamily/FourFunctions.lean
Modified
Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
Modified
Mathlib/Combinatorics/SetFamily/LYM.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Circulant.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Coloring.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean
Modified
Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
Modified
Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean
Modified
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
Modified
Mathlib/Computability/Ackermann.lean
Modified
Mathlib/Computability/AkraBazzi/AkraBazzi.lean
Modified
Mathlib/Computability/AkraBazzi/SumTransform.lean
Modified
Mathlib/Computability/Primrec/Basic.lean
Modified
Mathlib/Computability/Reduce.lean
Modified
Mathlib/Data/BitVec.lean
Modified
Mathlib/Data/Bool/Count.lean
Modified
Mathlib/Data/Complex/Basic.lean
Modified
Mathlib/Data/DFinsupp/Defs.lean
Modified
Mathlib/Data/ENat/Basic.lean
Modified
Mathlib/Data/ENat/Pow.lean
Modified
Mathlib/Data/EReal/Basic.lean
Modified
Mathlib/Data/Finset/Image.lean
Modified
Mathlib/Data/Finset/Interval.lean
Modified
Mathlib/Data/Finset/NatAntidiagonal.lean
Modified
Mathlib/Data/Finsupp/Antidiagonal.lean
deleted
def
Finsupp.antidiagonal'
Modified
Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
Modified
Mathlib/Data/Finsupp/Multiset.lean
deleted
def
Finsupp.orderIsoMultiset
deleted
def
Multiset.toFinsupp
deleted
def
Sym.equivNatSum
Modified
Mathlib/Data/Finsupp/Weight.lean
Modified
Mathlib/Data/Fintype/Units.lean
Modified
Mathlib/Data/Int/CardIntervalMod.lean
Modified
Mathlib/Data/Int/Fib/Basic.lean
Modified
Mathlib/Data/Int/Fib/Lemmas.lean
Modified
Mathlib/Data/Int/Star.lean
Modified
Mathlib/Data/List/Shortlex.lean
Modified
Mathlib/Data/Matrix/Basis.lean
Modified
Mathlib/Data/Matrix/Invertible.lean
Modified
Mathlib/Data/Multiset/Interval.lean
Modified
Mathlib/Data/NNRat/Defs.lean
Modified
Mathlib/Data/NNReal/Defs.lean
Modified
Mathlib/Data/Nat/Bitwise.lean
Modified
Mathlib/Data/Nat/Cast/Order/Ring.lean
Modified
Mathlib/Data/Nat/Choose/Central.lean
Modified
Mathlib/Data/Nat/Choose/Factorization.lean
Modified
Mathlib/Data/Nat/Choose/Multinomial.lean
deleted
def
Multiset.multinomial
Modified
Mathlib/Data/Nat/Choose/Sum.lean
Modified
Mathlib/Data/Nat/Choose/Vandermonde.lean
Modified
Mathlib/Data/Nat/Digits/Lemmas.lean
Modified
Mathlib/Data/Nat/Factorization/Basic.lean
Modified
Mathlib/Data/Nat/Factorization/Defs.lean
Modified
Mathlib/Data/Nat/Factorization/LCM.lean
Modified
Mathlib/Data/Nat/Factorization/Root.lean
Modified
Mathlib/Data/Nat/Fib/Basic.lean
Modified
Mathlib/Data/Nat/Fib/Zeckendorf.lean
Modified
Mathlib/Data/Nat/GCD/Basic.lean
Modified
Mathlib/Data/Nat/ModEq.lean
Modified
Mathlib/Data/Nat/Multiplicity.lean
Modified
Mathlib/Data/Nat/Prime/Defs.lean
Modified
Mathlib/Data/Nat/Squarefree.lean
Modified
Mathlib/Data/Nat/Totient.lean
Modified
Mathlib/Data/Num/Lemmas.lean
Modified
Mathlib/Data/Num/Prime.lean
Modified
Mathlib/Data/Num/ZNum.lean
Modified
Mathlib/Data/Ordmap/Ordset.lean
Modified
Mathlib/Data/PNat/Basic.lean
Modified
Mathlib/Data/Rat/Floor.lean
Modified
Mathlib/Data/Rat/NatSqrt/Defs.lean
Modified
Mathlib/Data/Real/Archimedean.lean
Modified
Mathlib/Data/Real/Embedding.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Setoid/Basic.lean
Modified
Mathlib/Data/Setoid/Partition.lean
Modified
Mathlib/Data/String/Basic.lean
Modified
Mathlib/Data/Sym/Basic.lean
Modified
Mathlib/Data/Vector/Basic.lean
modified
theorem
List.Vector.scanl_nil
Modified
Mathlib/Data/ZMod/Basic.lean
Modified
Mathlib/Data/ZMod/ValMinAbs.lean
Modified
Mathlib/Dynamics/Ergodic/AddCircle.lean
Modified
Mathlib/FieldTheory/Finite/Basic.lean
Modified
Mathlib/FieldTheory/Finite/Extension.lean
Modified
Mathlib/FieldTheory/Finite/GaloisField.lean
Modified
Mathlib/FieldTheory/Fixed.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
Modified
Mathlib/FieldTheory/IntermediateField/Basic.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
Modified
Mathlib/FieldTheory/IsPerfectClosure.lean
Modified
Mathlib/FieldTheory/JacobsonNoether.lean
Modified
Mathlib/FieldTheory/PolynomialGaloisGroup.lean
Modified
Mathlib/FieldTheory/RatFunc/Basic.lean
Modified
Mathlib/FieldTheory/RatFunc/Degree.lean
Modified
Mathlib/FieldTheory/SeparableDegree.lean
Modified
Mathlib/FieldTheory/SplittingField/Construction.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Sphere.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
Modified
Mathlib/Geometry/Euclidean/MongePoint.lean
Modified
Mathlib/Geometry/Euclidean/NinePointCircle.lean
Modified
Mathlib/Geometry/Euclidean/PerpBisector.lean
Modified
Mathlib/Geometry/Euclidean/Projection.lean
Modified
Mathlib/Geometry/Euclidean/Triangle.lean
Modified
Mathlib/Geometry/Group/Growth/LinearLowerBound.lean
Modified
Mathlib/Geometry/Manifold/HasGroupoid.lean
Modified
Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
Modified
Mathlib/Geometry/Manifold/IsManifold/Basic.lean
Modified
Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
Modified
Mathlib/Geometry/Manifold/PartitionOfUnity.lean
Modified
Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
Modified
Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
Modified
Mathlib/Geometry/RingedSpace/Basic.lean
Modified
Mathlib/Geometry/RingedSpace/OpenImmersion.lean
Modified
Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
added
structure
AlgebraicGeometry.PresheafedSpace.{u}
deleted
structure
AlgebraicGeometry.PresheafedSpace
Modified
Mathlib/Geometry/RingedSpace/SheafedSpace.lean
Modified
Mathlib/GroupTheory/ArchimedeanDensely.lean
Modified
Mathlib/GroupTheory/Commensurable.lean
Modified
Mathlib/GroupTheory/Commutator/Finite.lean
Modified
Mathlib/GroupTheory/CommutingProbability.lean
Modified
Mathlib/GroupTheory/Complement.lean
Modified
Mathlib/GroupTheory/Congruence/Hom.lean
Modified
Mathlib/GroupTheory/CoprodI.lean
Modified
Mathlib/GroupTheory/Coset/Basic.lean
Modified
Mathlib/GroupTheory/Coxeter/Basic.lean
Modified
Mathlib/GroupTheory/Divisible.lean
Modified
Mathlib/GroupTheory/DivisibleHull.lean
Modified
Mathlib/GroupTheory/Exponent.lean
Modified
Mathlib/GroupTheory/FreeAbelianGroup.lean
Modified
Mathlib/GroupTheory/FreeGroup/Basic.lean
Modified
Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
Modified
Mathlib/GroupTheory/GroupAction/Blocks.lean
Modified
Mathlib/GroupTheory/GroupAction/Defs.lean
Modified
Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
Modified
Mathlib/GroupTheory/GroupAction/Quotient.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
Modified
Mathlib/GroupTheory/HNNExtension.lean
Modified
Mathlib/GroupTheory/MonoidLocalization/Basic.lean
Modified
Mathlib/GroupTheory/Nilpotent.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/PushoutI.lean
Modified
Mathlib/GroupTheory/Schreier.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
Modified
Mathlib/GroupTheory/Subgroup/Centralizer.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Basis.lean
deleted
def
finsuppAffineCoords
Modified
Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
Modified
Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean
Modified
Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
Modified
Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
Modified
Mathlib/LinearAlgebra/Coevaluation.lean
Modified
Mathlib/LinearAlgebra/Complex/Module.lean
Modified
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
Modified
Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Int.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
Modified
Mathlib/LinearAlgebra/LinearPMap.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
Modified
Mathlib/LinearAlgebra/Matrix/Diagonal.lean
Modified
Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
Modified
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
Modified
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean
Modified
Mathlib/LinearAlgebra/Matrix/Notation.lean
Modified
Mathlib/LinearAlgebra/Matrix/RowCol.lean
Modified
Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLin.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
Modified
Mathlib/LinearAlgebra/Matrix/Trace.lean
Modified
Mathlib/LinearAlgebra/Matrix/Transvection.lean
Modified
Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/PID.lean
Modified
Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
Modified
Mathlib/LinearAlgebra/Pi.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Dual.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/Reflection.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Base.lean
Modified
Mathlib/LinearAlgebra/RootSystem/BaseExists.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Chain.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Relations.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean
Modified
Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean
Modified
Mathlib/LinearAlgebra/SymplecticGroup.lean
Modified
Mathlib/LinearAlgebra/TensorPower/Basic.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Basis.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Defs.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
Modified
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
Modified
Mathlib/MeasureTheory/Constructions/Pi.lean
Modified
Mathlib/MeasureTheory/Covering/Besicovitch.lean
Modified
Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
Modified
Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
Modified
Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean
Modified
Mathlib/MeasureTheory/Function/Jacobian.lean
Modified
Mathlib/MeasureTheory/Function/JacobianOneDim.lean
Modified
Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
deleted
def
MeasureTheory.Lp.boundedContinuousFunction
Modified
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
Modified
Mathlib/MeasureTheory/Integral/CircleAverage.lean
Modified
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
Modified
Mathlib/MeasureTheory/Integral/CircleTransform.lean
Modified
Mathlib/MeasureTheory/Integral/CompactlySupported.lean
Modified
Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean
Modified
Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
Modified
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalAverage.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean
Modified
Mathlib/MeasureTheory/Integral/Layercake.lean
Modified
Mathlib/MeasureTheory/Integral/Prod.lean
Modified
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean
Modified
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean
Modified
Mathlib/MeasureTheory/Integral/SetToL1.lean
Modified
Mathlib/MeasureTheory/Integral/TorusIntegral.lean
Modified
Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
Modified
Mathlib/MeasureTheory/Measure/DiracProba.lean
Modified
Mathlib/MeasureTheory/Measure/EverywherePos.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
Modified
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Prod.lean
Modified
Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Tight.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Basic.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean
Modified
Mathlib/ModelTheory/Complexity.lean
Modified
Mathlib/ModelTheory/DirectLimit.lean
Modified
Mathlib/ModelTheory/Order.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/ModelTheory/Syntax.lean
Modified
Mathlib/ModelTheory/Ultraproducts.lean
Modified
Mathlib/NumberTheory/ADEInequality.lean
Modified
Mathlib/NumberTheory/AbelSummation.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Misc.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/VonMangoldt.lean
Modified
Mathlib/NumberTheory/Bernoulli.lean
Modified
Mathlib/NumberTheory/BernoulliPolynomials.lean
Modified
Mathlib/NumberTheory/Bertrand.lean
Modified
Mathlib/NumberTheory/Chebyshev.lean
Modified
Mathlib/NumberTheory/ClassNumber/Finite.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Basic.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
Modified
Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
Modified
Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
Modified
Mathlib/NumberTheory/Divisors.lean
Modified
Mathlib/NumberTheory/FLT/Basic.lean
Modified
Mathlib/NumberTheory/FactorisationProperties.lean
Modified
Mathlib/NumberTheory/Fermat.lean
Modified
Mathlib/NumberTheory/FermatPsp.lean
Modified
Mathlib/NumberTheory/Harmonic/Bounds.lean
Modified
Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
Modified
Mathlib/NumberTheory/LSeries/Convolution.lean
Modified
Mathlib/NumberTheory/LSeries/Dirichlet.lean
Modified
Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
Modified
Mathlib/NumberTheory/LSeries/Linearity.lean
Modified
Mathlib/NumberTheory/LSeries/Nonvanishing.lean
Modified
Mathlib/NumberTheory/LSeries/PrimesInAP.lean
Modified
Mathlib/NumberTheory/LSeries/SumCoeff.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
Modified
Mathlib/NumberTheory/LocalField/Basic.lean
Modified
Mathlib/NumberTheory/LucasLehmer.lean
Modified
Mathlib/NumberTheory/MaricaSchoenheim.lean
Modified
Mathlib/NumberTheory/Modular.lean
Modified
Mathlib/NumberTheory/ModularForms/Basic.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean
Modified
Mathlib/NumberTheory/ModularForms/Identities.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
Modified
Mathlib/NumberTheory/ModularForms/NormTrace.lean
Modified
Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean
Modified
Mathlib/NumberTheory/MulChar/Lemmas.lean
Modified
Mathlib/NumberTheory/Multiplicity.lean
Modified
Mathlib/NumberTheory/NumberField/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/CMField.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/PID.lean
Modified
Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
Modified
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
Modified
Mathlib/NumberTheory/NumberField/House.lean
Modified
Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean
Modified
Mathlib/NumberTheory/NumberField/Units/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Units/Regulator.lean
Modified
Mathlib/NumberTheory/Padics/AddChar.lean
Modified
Mathlib/NumberTheory/Padics/Hensel.lean
Modified
Mathlib/NumberTheory/Padics/MahlerBasis.lean
Modified
Mathlib/NumberTheory/Padics/PadicIntegers.lean
Modified
Mathlib/NumberTheory/Padics/PadicNorm.lean
Modified
Mathlib/NumberTheory/Padics/RingHoms.lean
Modified
Mathlib/NumberTheory/Padics/WithVal.lean
Modified
Mathlib/NumberTheory/Pell.lean
Modified
Mathlib/NumberTheory/PellMatiyasevic.lean
Modified
Mathlib/NumberTheory/Primorial.lean
Modified
Mathlib/NumberTheory/PythagoreanTriples.lean
Modified
Mathlib/NumberTheory/Real/GoldenRatio.lean
Modified
Mathlib/NumberTheory/Real/Irrational.lean
Modified
Mathlib/NumberTheory/SiegelsLemma.lean
Modified
Mathlib/NumberTheory/SmoothNumbers.lean
Modified
Mathlib/NumberTheory/SumFourSquares.lean
Modified
Mathlib/NumberTheory/SumPrimeReciprocals.lean
Modified
Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean
Modified
Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
Modified
Mathlib/NumberTheory/WellApproximable.lean
Modified
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
Modified
Mathlib/Order/Birkhoff.lean
Modified
Mathlib/Order/BooleanAlgebra/Basic.lean
modified
theorem
himp_le
Modified
Mathlib/Order/CompleteSublattice.lean
Modified
Mathlib/Order/Copy.lean
Modified
Mathlib/Order/Filter/Cocardinal.lean
Modified
Mathlib/Order/Lattice/Congruence.lean
Modified
Mathlib/Order/SuccPred/Archimedean.lean
Modified
Mathlib/Order/SuccPred/LinearLocallyFinite.lean
Modified
Mathlib/Probability/Distributions/Beta.lean
Modified
Mathlib/Probability/Distributions/Exponential.lean
Modified
Mathlib/Probability/Distributions/Fernique.lean
Modified
Mathlib/Probability/Distributions/Gamma.lean
Modified
Mathlib/Probability/Distributions/Gaussian/Fernique.lean
Modified
Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean
Modified
Mathlib/Probability/Distributions/Gaussian/Real.lean
Modified
Mathlib/Probability/Distributions/Uniform.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean
Modified
Mathlib/Probability/Kernel/Irreducible.lean
Modified
Mathlib/Probability/Kernel/RadonNikodym.lean
Modified
Mathlib/Probability/Moments/Basic.lean
Modified
Mathlib/Probability/Moments/SubGaussian.lean
Modified
Mathlib/Probability/ProductMeasure.lean
Modified
Mathlib/Probability/StrongLaw.lean
Modified
Mathlib/RepresentationTheory/Coinvariants.lean
Modified
Mathlib/RepresentationTheory/FinGroupCharZero.lean
Modified
Mathlib/RepresentationTheory/FiniteIndex.lean
Modified
Mathlib/RepresentationTheory/Rep.lean
Modified
Mathlib/RepresentationTheory/Tannaka.lean
Modified
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
Modified
Mathlib/RingTheory/AdicCompletion/Functoriality.lean
modified
def
AdicCompletion.map
Modified
Mathlib/RingTheory/AdicCompletion/Topology.lean
Modified
Mathlib/RingTheory/AdjoinRoot.lean
Modified
Mathlib/RingTheory/Algebraic/Integral.lean
Modified
Mathlib/RingTheory/Bialgebra/TensorProduct.lean
Modified
Mathlib/RingTheory/Binomial.lean
Modified
Mathlib/RingTheory/Coalgebra/Basic.lean
Modified
Mathlib/RingTheory/Coalgebra/Convolution.lean
Modified
Mathlib/RingTheory/Coalgebra/TensorProduct.lean
Modified
Mathlib/RingTheory/Conductor.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DedekindDomain/Different.lean
Modified
Mathlib/RingTheory/DedekindDomain/Factorization.lean
Modified
Mathlib/RingTheory/Derivation/Basic.lean
Modified
Mathlib/RingTheory/Discriminant.lean
Modified
Mathlib/RingTheory/DividedPowers/RatAlgebra.lean
Modified
Mathlib/RingTheory/Etale/QuasiFinite.lean
Modified
Mathlib/RingTheory/Etale/StandardEtale.lean
Modified
Mathlib/RingTheory/Extension/Generators.lean
deleted
def
Algebra.Generators.ofAlgEquiv
Modified
Mathlib/RingTheory/Extension/Presentation/Basic.lean
deleted
def
Algebra.Presentation.ofAlgEquiv
deleted
def
Algebra.Presentation.quotientEquiv
Modified
Mathlib/RingTheory/Extension/Presentation/Submersive.lean
deleted
def
Algebra.PreSubmersivePresentation.ofAlgEquiv
deleted
def
Algebra.SubmersivePresentation.ofAlgEquiv
Modified
Mathlib/RingTheory/Finiteness/ModuleFinitePresentation.lean
Modified
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
Modified
Mathlib/RingTheory/HahnSeries/Binomial.lean
Modified
Mathlib/RingTheory/HopfAlgebra/Basic.lean
Modified
Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
Modified
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/ChineseRemainder.lean
Modified
Mathlib/RingTheory/Idempotents.lean
Modified
Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
Modified
Mathlib/RingTheory/Kaehler/Basic.lean
Modified
Mathlib/RingTheory/Kaehler/JacobiZariski.lean
Modified
Mathlib/RingTheory/Kaehler/Polynomial.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/LocalProperties/Projective.lean
Modified
Mathlib/RingTheory/LocalRing/Module.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean
Modified
Mathlib/RingTheory/Localization/Basic.lean
Modified
Mathlib/RingTheory/Localization/Integral.lean
Modified
Mathlib/RingTheory/MvPolynomial.lean
Modified
Mathlib/RingTheory/MvPolynomial/Groebner.lean
Modified
Mathlib/RingTheory/MvPolynomial/Ideal.lean
deleted
def
MvPolynomial.idealOfVars
Modified
Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean
Modified
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
deleted
def
MonomialOrder.degree
deleted
def
MonomialOrder.leadingCoeff
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Basic.lean
Modified
Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
deleted
def
MvPowerSeries.LinearTopology.basis
Modified
Mathlib/RingTheory/Nakayama.lean
Modified
Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean
Modified
Mathlib/RingTheory/NoetherNormalization.lean
Modified
Mathlib/RingTheory/NormalClosure.lean
Modified
Mathlib/RingTheory/Perfectoid/Untilt.lean
Modified
Mathlib/RingTheory/Polynomial/Bernstein.lean
Modified
Mathlib/RingTheory/Polynomial/Chebyshev.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean
Modified
Mathlib/RingTheory/Polynomial/IsIntegral.lean
Modified
Mathlib/RingTheory/Polynomial/Pochhammer.lean
Modified
Mathlib/RingTheory/Polynomial/Resultant/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/ScaleRoots.lean
Modified
Mathlib/RingTheory/Polynomial/SeparableDegree.lean
Modified
Mathlib/RingTheory/Polynomial/ShiftedLegendre.lean
Modified
Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
Modified
Mathlib/RingTheory/PowerBasis.lean
Modified
Mathlib/RingTheory/PowerSeries/Exp.lean
Modified
Mathlib/RingTheory/PowerSeries/Restricted.lean
Modified
Mathlib/RingTheory/QuasiFinite/Basic.lean
Modified
Mathlib/RingTheory/QuasiFinite/Polynomial.lean
Modified
Mathlib/RingTheory/Smooth/Fiber.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
Modified
Mathlib/RingTheory/TensorProduct/Basic.lean
Modified
Mathlib/RingTheory/TensorProduct/Free.lean
Modified
Mathlib/RingTheory/Trace/Basic.lean
Modified
Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
Modified
Mathlib/RingTheory/Unramified/LocalRing.lean
Modified
Mathlib/RingTheory/Unramified/LocalStructure.lean
Modified
Mathlib/RingTheory/Valuation/Discrete/Basic.lean
Modified
Mathlib/RingTheory/WittVector/Frobenius.lean
Modified
Mathlib/RingTheory/WittVector/IsPoly.lean
Modified
Mathlib/RingTheory/WittVector/StructurePolynomial.lean
Modified
Mathlib/RingTheory/WittVector/Teichmuller.lean
Modified
Mathlib/RingTheory/WittVector/WittPolynomial.lean
Modified
Mathlib/RingTheory/ZariskisMainTheorem.lean
Modified
Mathlib/SetTheory/Lists.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean
Modified
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean
Modified
Mathlib/Tactic/FieldSimp/Lemmas.lean
Modified
Mathlib/Tactic/Module.lean
Modified
Mathlib/Tactic/NormNum/Abs.lean
Modified
Mathlib/Tactic/NormNum/Basic.lean
Modified
Mathlib/Tactic/NormNum/Eq.lean
Modified
Mathlib/Tactic/NormNum/GCD.lean
Modified
Mathlib/Tactic/NormNum/Ineq.lean
Modified
Mathlib/Tactic/NormNum/Inv.lean
Modified
Mathlib/Tactic/NormNum/Irrational.lean
Modified
Mathlib/Tactic/NormNum/LegendreSymbol.lean
Modified
Mathlib/Tactic/NormNum/NatSqrt.lean
Modified
Mathlib/Tactic/NormNum/Pow.lean
Modified
Mathlib/Tactic/NormNum/PowMod.lean
Modified
Mathlib/Tactic/NormNum/RealSqrt.lean
Modified
Mathlib/Tactic/NormNum/Result.lean
Modified
Mathlib/Tactic/Ring/Common.lean
Modified
Mathlib/Tactic/SimpIntro.lean
Modified
Mathlib/Tactic/Translate/Core.lean
Modified
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
Modified
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Completion.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
Modified
Mathlib/Topology/Algebra/IsUniformGroup/DiscreteSubgroup.lean
Modified
Mathlib/Topology/Algebra/Module/Equiv.lean
Modified
Mathlib/Topology/Algebra/Module/LinearMap.lean
Modified
Mathlib/Topology/Algebra/Polynomial.lean
Modified
Mathlib/Topology/Algebra/Ring/Real.lean
Modified
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
Modified
Mathlib/Topology/Algebra/Valued/NormedValued.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
Modified
Mathlib/Topology/Category/Profinite/Nobeling/Span.lean
Modified
Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean
Modified
Mathlib/Topology/Connected/PathConnected.lean
Modified
Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean
deleted
def
compactlySupported
Modified
Mathlib/Topology/ContinuousMap/CompactlySupported.lean
Modified
Mathlib/Topology/Covering/AddCircle.lean
Modified
Mathlib/Topology/Homotopy/Basic.lean
Modified
Mathlib/Topology/Homotopy/HSpaces.lean
Modified
Mathlib/Topology/Homotopy/HomotopyGroup.lean
Modified
Mathlib/Topology/Homotopy/Path.lean
Modified
Mathlib/Topology/Instances/AddCircle/Defs.lean
Modified
Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean
Modified
Mathlib/Topology/Instances/CantorSet.lean
Modified
Mathlib/Topology/Instances/EReal/Lemmas.lean
Modified
Mathlib/Topology/Instances/Int.lean
Modified
Mathlib/Topology/Instances/Real/Lemmas.lean
Modified
Mathlib/Topology/IsClosedRestrict.lean
Modified
Mathlib/Topology/LocalAtTarget.lean
Modified
Mathlib/Topology/MetricSpace/Basic.lean
Modified
Mathlib/Topology/MetricSpace/Contracting.lean
Modified
Mathlib/Topology/MetricSpace/Dilation.lean
Modified
Mathlib/Topology/MetricSpace/GromovHausdorff.lean
Modified
Mathlib/Topology/MetricSpace/HausdorffDistance.lean
Modified
Mathlib/Topology/MetricSpace/Lipschitz.lean
Modified
Mathlib/Topology/MetricSpace/PiNat.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
Modified
Mathlib/Topology/OpenPartialHomeomorph/Basic.lean
Modified
Mathlib/Topology/Order/ScottTopology.lean
Modified
Mathlib/Topology/Path.lean
Modified
Mathlib/Topology/Separation/CompletelyRegular.lean
Modified
Mathlib/Topology/Subpath.lean
Modified
Mathlib/Topology/UnitInterval.lean
Modified
Mathlib/Topology/UrysohnsLemma.lean
Modified
MathlibTest/Algebra/Category/Grp/Injective.lean
Modified
MathlibTest/FieldSimp.lean
Modified
MathlibTest/GCongr/inequalities.lean
Modified
MathlibTest/fast_instance.lean
Modified
MathlibTest/hintAll.lean
Modified
MathlibTest/matrix.lean
Modified
MathlibTest/push.lean
Modified
MathlibTest/toAdditive.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain