Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-07-16 01:47
79d0395a
View on Github →
chore: bump toolchain to v4.33.0-rc1 (
#41779
)
Estimated changes
Modified
Archive/Hairer.lean
Modified
Archive/Imo/Imo1987Q1.lean
Modified
Archive/Imo/Imo2013Q1.lean
Modified
Archive/Imo/Imo2019Q2.lean
Modified
Archive/Imo/Imo2024Q5.lean
Modified
Archive/MinimalSheffer.lean
Modified
Archive/Sensitivity.lean
Modified
Archive/Wiedijk100Theorems/FriendshipGraphs.lean
Modified
Archive/Wiedijk100Theorems/Konigsberg.lean
Modified
Archive/ZagierTwoSquares.lean
Modified
Cache/Hashing.lean
Modified
Cache/IO.lean
modified
def
Cache.IO.rootHashGeneration
Modified
Counterexamples/AharoniKorman.lean
Modified
Counterexamples/MapFloor.lean
Modified
Counterexamples/Phillips.lean
Modified
Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean
Modified
Mathlib/Algebra/Algebra/Epi.lean
Modified
Mathlib/Algebra/Algebra/Equiv.lean
Modified
Mathlib/Algebra/Algebra/NonUnitalHom.lean
Modified
Mathlib/Algebra/Algebra/Operations.lean
Modified
Mathlib/Algebra/Algebra/Opposite.lean
Modified
Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
Modified
Mathlib/Algebra/Algebra/ZMod.lean
Modified
Mathlib/Algebra/BigOperators/Expect.lean
Modified
Mathlib/Algebra/BigOperators/Fin.lean
Modified
Mathlib/Algebra/BigOperators/Finprod.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean
Modified
Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
Modified
Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
Modified
Mathlib/Algebra/BrauerGroup/Defs.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Basic.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Colimits.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Limits.lean
Modified
Mathlib/Algebra/Category/Grp/Abelian.lean
Modified
Mathlib/Algebra/Category/Grp/Colimits.lean
Modified
Mathlib/Algebra/Category/Grp/EpiMono.lean
Modified
Mathlib/Algebra/Category/Grp/Images.lean
Modified
Mathlib/Algebra/Category/Grp/Limits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Abelian.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Descent.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
Modified
Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
Modified
Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Images.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Adjunction.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/ColimitFunctor.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Stalk.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Ulift.lean
Modified
Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/MonCat/Limits.lean
Modified
Mathlib/Algebra/Category/Ring/Adjunctions.lean
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
Modified
Mathlib/Algebra/Category/Ring/FinitePresentation.lean
Modified
Mathlib/Algebra/Category/Ring/Under/Basic.lean
Modified
Mathlib/Algebra/Category/Ring/Under/Property.lean
Modified
Mathlib/Algebra/Central/Basic.lean
Modified
Mathlib/Algebra/CharP/Invertible.lean
Modified
Mathlib/Algebra/CharP/MixedCharZero.lean
Modified
Mathlib/Algebra/Colimit/DirectLimit.lean
Modified
Mathlib/Algebra/Colimit/Finiteness.lean
Modified
Mathlib/Algebra/Colimit/Module.lean
Modified
Mathlib/Algebra/Colimit/Ring.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
Modified
Mathlib/Algebra/DirectSum/Basic.lean
Modified
Mathlib/Algebra/DirectSum/Decomposition.lean
Modified
Mathlib/Algebra/DirectSum/Idempotents.lean
Modified
Mathlib/Algebra/DirectSum/Internal.lean
Modified
Mathlib/Algebra/DirectSum/LinearMap.lean
Modified
Mathlib/Algebra/DirectSum/Module.lean
Modified
Mathlib/Algebra/DirectSum/Ring.lean
Modified
Mathlib/Algebra/DualQuaternion.lean
Modified
Mathlib/Algebra/Exact/Basic.lean
Modified
Mathlib/Algebra/Expr.lean
Modified
Mathlib/Algebra/Field/IsField.lean
Modified
Mathlib/Algebra/Field/Rat.lean
Modified
Mathlib/Algebra/Free.lean
Modified
Mathlib/Algebra/FreeAlgebra.lean
Modified
Mathlib/Algebra/FreeMonoid/Basic.lean
Modified
Mathlib/Algebra/GCDMonoid/Basic.lean
Modified
Mathlib/Algebra/GradedMonoid.lean
Modified
Mathlib/Algebra/Group/Action/Basic.lean
Modified
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean
Modified
Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean
Modified
Mathlib/Algebra/Group/Conj.lean
Modified
Mathlib/Algebra/Group/End.lean
Modified
Mathlib/Algebra/Group/Finsupp.lean
Modified
Mathlib/Algebra/Group/Hom/Basic.lean
Modified
Mathlib/Algebra/Group/Hom/Defs.lean
Modified
Mathlib/Algebra/Group/Invertible/Basic.lean
Modified
Mathlib/Algebra/Group/Invertible/Defs.lean
Modified
Mathlib/Algebra/Group/Pi/Basic.lean
Modified
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
Modified
Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean
Modified
Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
Modified
Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean
Modified
Mathlib/Algebra/Group/Subgroup/Basic.lean
Modified
Mathlib/Algebra/Group/Subgroup/Ker.lean
Modified
Mathlib/Algebra/Group/Subgroup/Map.lean
Modified
Mathlib/Algebra/Group/Subgroup/Pointwise.lean
Modified
Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
Modified
Mathlib/Algebra/Group/Submonoid/Operations.lean
Modified
Mathlib/Algebra/Group/Submonoid/Pointwise.lean
Modified
Mathlib/Algebra/Group/Units/Defs.lean
Modified
Mathlib/Algebra/Group/WithOne/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/Associated.lean
Modified
Mathlib/Algebra/GroupWithZero/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/Indicator.lean
Modified
Mathlib/Algebra/GroupWithZero/InjSurj.lean
Modified
Mathlib/Algebra/GroupWithZero/Invertible.lean
Modified
Mathlib/Algebra/GroupWithZero/ProdHom.lean
Modified
Mathlib/Algebra/GroupWithZero/Range.lean
Modified
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/WithZero.lean
Modified
Mathlib/Algebra/Homology/Additive.lean
Modified
Mathlib/Algebra/Homology/Augment.lean
Modified
Mathlib/Algebra/Homology/BifunctorAssociator.lean
Modified
Mathlib/Algebra/Homology/BifunctorShift.lean
Modified
Mathlib/Algebra/Homology/CochainComplexOpposite.lean
Modified
Mathlib/Algebra/Homology/CommSq.lean
Modified
Mathlib/Algebra/Homology/ComplexShape.lean
Modified
Mathlib/Algebra/Homology/ComplexShapeSigns.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/DerivabilityStructureInjectives.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/TStructure.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Fractions.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/SmallShiftedHom.lean
Modified
Mathlib/Algebra/Homology/DifferentialObject.lean
Modified
Mathlib/Algebra/Homology/Embedding/Basic.lean
Modified
Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
Modified
Mathlib/Algebra/Homology/Embedding/Connect.lean
Modified
Mathlib/Algebra/Homology/Embedding/Extend.lean
Modified
Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
Modified
Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean
Modified
Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
Modified
Mathlib/Algebra/Homology/Embedding/Restriction.lean
Modified
Mathlib/Algebra/Homology/Embedding/RestrictionHomology.lean
Modified
Mathlib/Algebra/Homology/Embedding/TruncGE.lean
Modified
Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
Modified
Mathlib/Algebra/Homology/Embedding/TruncLE.lean
Modified
Mathlib/Algebra/Homology/Factorizations/CM5a.lean
Modified
Mathlib/Algebra/Homology/Factorizations/CM5b.lean
Modified
Mathlib/Algebra/Homology/HomologicalBicomplex.lean
Modified
Mathlib/Algebra/Homology/HomologicalComplex.lean
Modified
Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
Modified
Mathlib/Algebra/Homology/HomologySequence.lean
Modified
Mathlib/Algebra/Homology/HomologySequenceLemmas.lean
Modified
Mathlib/Algebra/Homology/Homotopy.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplexCohomology.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/KProjective.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
Modified
Mathlib/Algebra/Homology/HomotopyCofiber.lean
Modified
Mathlib/Algebra/Homology/LeftResolution/Basic.lean
Modified
Mathlib/Algebra/Homology/LeftResolution/Reduced.lean
Modified
Mathlib/Algebra/Homology/LeftResolution/Transport.lean
Modified
Mathlib/Algebra/Homology/Localization.lean
Modified
Mathlib/Algebra/Homology/ModelCategory/Lifting.lean
Modified
Mathlib/Algebra/Homology/Monoidal.lean
Modified
Mathlib/Algebra/Homology/Opposite.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Ab.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Basic.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Homology.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Limits.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
Modified
Mathlib/Algebra/Homology/Single.lean
Modified
Mathlib/Algebra/Homology/SingleHomology.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/Basic.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/Page.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean
Modified
Mathlib/Algebra/Homology/TotalComplex.lean
Modified
Mathlib/Algebra/Homology/TotalComplexShift.lean
Modified
Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
Modified
Mathlib/Algebra/Jordan/Basic.lean
Modified
Mathlib/Algebra/Lie/Abelian.lean
Modified
Mathlib/Algebra/Lie/AdjointAction/Basic.lean
Modified
Mathlib/Algebra/Lie/BaseChange.lean
Modified
Mathlib/Algebra/Lie/Basic.lean
Modified
Mathlib/Algebra/Lie/Basis.lean
Modified
Mathlib/Algebra/Lie/Classical.lean
Modified
Mathlib/Algebra/Lie/Derivation/Basic.lean
Modified
Mathlib/Algebra/Lie/DirectSum.lean
Modified
Mathlib/Algebra/Lie/EngelSubalgebra.lean
Modified
Mathlib/Algebra/Lie/Extension.lean
Modified
Mathlib/Algebra/Lie/Graded.lean
Modified
Mathlib/Algebra/Lie/LieTheorem.lean
Modified
Mathlib/Algebra/Lie/Matrix.lean
Modified
Mathlib/Algebra/Lie/OfAssociative.lean
Modified
Mathlib/Algebra/Lie/Quotient.lean
Modified
Mathlib/Algebra/Lie/SemiDirect.lean
Modified
Mathlib/Algebra/Lie/Solvable.lean
Modified
Mathlib/Algebra/Lie/Submodule.lean
Modified
Mathlib/Algebra/Lie/TensorProduct.lean
Modified
Mathlib/Algebra/Lie/UniversalEnveloping.lean
Modified
Mathlib/Algebra/Lie/Weights/Basic.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/Module/CharacterModule.lean
Modified
Mathlib/Algebra/Module/Equiv/Basic.lean
Modified
Mathlib/Algebra/Module/Equiv/Defs.lean
Modified
Mathlib/Algebra/Module/GradedModule.lean
Modified
Mathlib/Algebra/Module/Injective.lean
Modified
Mathlib/Algebra/Module/Lattice.lean
Modified
Mathlib/Algebra/Module/LinearMap/Defs.lean
Modified
Mathlib/Algebra/Module/LinearMap/Index.lean
Modified
Mathlib/Algebra/Module/LinearMap/Polynomial.lean
Modified
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
Modified
Mathlib/Algebra/Module/NatInt.lean
Modified
Mathlib/Algebra/Module/PID.lean
Modified
Mathlib/Algebra/Module/Presentation/Cokernel.lean
Modified
Mathlib/Algebra/Module/Presentation/Differentials.lean
Modified
Mathlib/Algebra/Module/Presentation/DirectSum.lean
Modified
Mathlib/Algebra/Module/SnakeLemma.lean
Modified
Mathlib/Algebra/Module/Submodule/Bilinear.lean
Modified
Mathlib/Algebra/Module/Submodule/Defs.lean
Modified
Mathlib/Algebra/Module/Submodule/Invariant.lean
Modified
Mathlib/Algebra/Module/Submodule/Ker.lean
Modified
Mathlib/Algebra/Module/Submodule/LinearMap.lean
Modified
Mathlib/Algebra/Module/Submodule/Map.lean
Modified
Mathlib/Algebra/Module/Submodule/Range.lean
Modified
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
Modified
Mathlib/Algebra/Module/Torsion/Basic.lean
Modified
Mathlib/Algebra/Module/TransferInstance.lean
Modified
Mathlib/Algebra/Module/ZLattice/Covolume.lean
Modified
Mathlib/Algebra/Module/ZLattice/Summable.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Defs.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Degree.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Grading.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Lift.lean
Modified
Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Module.lean
Modified
Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean
Modified
Mathlib/Algebra/MonoidAlgebra/PointwiseSMul.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Support.lean
Modified
Mathlib/Algebra/MvPolynomial/Basic.lean
Modified
Mathlib/Algebra/MvPolynomial/CommRing.lean
Modified
Mathlib/Algebra/MvPolynomial/Degrees.lean
Modified
Mathlib/Algebra/MvPolynomial/Equiv.lean
Modified
Mathlib/Algebra/MvPolynomial/Eval.lean
Modified
Mathlib/Algebra/MvPolynomial/Rename.lean
Modified
Mathlib/Algebra/MvPolynomial/Variables.lean
Modified
Mathlib/Algebra/Opposites.lean
Modified
Mathlib/Algebra/Order/Antidiag/Finsupp.lean
Modified
Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean
Modified
Mathlib/Algebra/Order/Antidiag/Nat.lean
Modified
Mathlib/Algebra/Order/Antidiag/Pi.lean
Modified
Mathlib/Algebra/Order/Antidiag/Prod.lean
Modified
Mathlib/Algebra/Order/Archimedean/Basic.lean
Modified
Mathlib/Algebra/Order/Archimedean/Class.lean
Modified
Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
Modified
Mathlib/Algebra/Order/CompleteField.lean
Modified
Mathlib/Algebra/Order/Floor/Defs.lean
Modified
Mathlib/Algebra/Order/Group/Lattice.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Lex.lean
Modified
Mathlib/Algebra/Order/Hom/MonoidWithZero.lean
Modified
Mathlib/Algebra/Order/Interval/Basic.lean
Modified
Mathlib/Algebra/Order/IsBotOne.lean
Modified
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
Modified
Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
Modified
Mathlib/Algebra/Order/Ring/StandardPart.lean
Modified
Mathlib/Algebra/Polynomial/Basic.lean
Modified
Mathlib/Algebra/Polynomial/BigOperators.lean
Modified
Mathlib/Algebra/Polynomial/Bivariate.lean
Modified
Mathlib/Algebra/Polynomial/Coeff.lean
Modified
Mathlib/Algebra/Polynomial/Degree/Defs.lean
Modified
Mathlib/Algebra/Polynomial/Derivation.lean
Modified
Mathlib/Algebra/Polynomial/Expand.lean
Modified
Mathlib/Algebra/Polynomial/Laurent.lean
Modified
Mathlib/Algebra/Polynomial/Module/AEval.lean
Modified
Mathlib/Algebra/Polynomial/Module/Basic.lean
Modified
Mathlib/Algebra/Polynomial/OfFn.lean
Modified
Mathlib/Algebra/Polynomial/Reverse.lean
Modified
Mathlib/Algebra/Polynomial/Splits.lean
Modified
Mathlib/Algebra/QuadraticAlgebra/Basic.lean
Modified
Mathlib/Algebra/Quandle.lean
Modified
Mathlib/Algebra/Quaternion.lean
Modified
Mathlib/Algebra/Ring/CentroidHom.lean
Modified
Mathlib/Algebra/Ring/Equiv.lean
Modified
Mathlib/Algebra/Ring/Hom/Defs.lean
Modified
Mathlib/Algebra/Ring/Invertible.lean
Modified
Mathlib/Algebra/Ring/Subring/Basic.lean
Modified
Mathlib/Algebra/RingQuot.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/Star/CentroidHom.lean
Modified
Mathlib/Algebra/Star/Module.lean
Modified
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Star/RingQuot.lean
Modified
Mathlib/Algebra/Star/StarAlgHom.lean
Modified
Mathlib/Algebra/Star/UnitaryStarAlgAut.lean
Modified
Mathlib/Algebra/Symmetrized.lean
Modified
Mathlib/Algebra/TrivSqZeroExt/Basic.lean
Modified
Mathlib/Algebra/TrivSqZeroExt/Ideal.lean
Modified
Mathlib/AlgebraicGeometry/AffineScheme.lean
Modified
Mathlib/AlgebraicGeometry/AffineSpace.lean
Modified
Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean
Modified
Mathlib/AlgebraicGeometry/AlgClosed/Basic.lean
Modified
Mathlib/AlgebraicGeometry/Artinian.lean
Modified
Mathlib/AlgebraicGeometry/Birational/Birational.lean
Modified
Mathlib/AlgebraicGeometry/Birational/Composition.lean
Modified
Mathlib/AlgebraicGeometry/Birational/RationalMap.lean
Modified
Mathlib/AlgebraicGeometry/Cover/Directed.lean
Modified
Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean
Modified
Mathlib/AlgebraicGeometry/Cover/Open.lean
Modified
Mathlib/AlgebraicGeometry/Cover/Over.lean
Modified
Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
Modified
Mathlib/AlgebraicGeometry/Fiber.lean
Modified
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
Modified
Mathlib/AlgebraicGeometry/Geometrically/Basic.lean
Modified
Mathlib/AlgebraicGeometry/Geometrically/Connected.lean
Modified
Mathlib/AlgebraicGeometry/Geometrically/Integral.lean
Modified
Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean
Modified
Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean
Modified
Mathlib/AlgebraicGeometry/Gluing.lean
Modified
Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean
Modified
Mathlib/AlgebraicGeometry/IdealSheaf/Functorial.lean
Modified
Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean
Modified
Mathlib/AlgebraicGeometry/Limits.lean
Modified
Mathlib/AlgebraicGeometry/Modules/Sheaf.lean
Modified
Mathlib/AlgebraicGeometry/Modules/Tilde.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Descent.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Etale.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Finite.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Flat.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FlatDescent.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FlatMono.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/LocalClosure.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/WeaklyEtale.lean
Modified
Mathlib/AlgebraicGeometry/Noetherian.lean
Modified
Mathlib/AlgebraicGeometry/Normalization.lean
Modified
Mathlib/AlgebraicGeometry/OpenImmersion.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Functor.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
Modified
Mathlib/AlgebraicGeometry/Properties.lean
Modified
Mathlib/AlgebraicGeometry/PullbackCarrier.lean
Modified
Mathlib/AlgebraicGeometry/Pullbacks.lean
Modified
Mathlib/AlgebraicGeometry/QuasiAffine.lean
Modified
Mathlib/AlgebraicGeometry/RelativeGluing.lean
Modified
Mathlib/AlgebraicGeometry/ResidueField.lean
Modified
Mathlib/AlgebraicGeometry/Restrict.lean
Modified
Mathlib/AlgebraicGeometry/Scheme.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Affine.lean
Modified
Mathlib/AlgebraicGeometry/Sites/AffineEtale.lean
Modified
Mathlib/AlgebraicGeometry/Sites/BigZariski.lean
Modified
Mathlib/AlgebraicGeometry/Sites/ConstantSheaf.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Etale.lean
Modified
Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Fpqc.lean
Modified
Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Proetale.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Representability.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Small.lean
Modified
Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
Modified
Mathlib/AlgebraicGeometry/Spec.lean
Modified
Mathlib/AlgebraicGeometry/SpreadingOut.lean
Modified
Mathlib/AlgebraicGeometry/Stalk.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
Modified
Mathlib/AlgebraicGeometry/ZariskisMainTheorem.lean
Modified
Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
Modified
Mathlib/AlgebraicTopology/CechNerve.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
Modified
Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
Modified
Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Basic.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/BifibrantObjectHomotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/CofibrantObjectHomotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Cylinder.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Transport.lean
Modified
Mathlib/AlgebraicTopology/MooreComplex.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/DeltaZeroIter.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/Rev.lean
Modified
Mathlib/AlgebraicTopology/SimplicialNerve.lean
Modified
Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplicialObject/Coskeletal.lean
Modified
Mathlib/AlgebraicTopology/SimplicialObject/DeltaZeroIter.lean
Modified
Mathlib/AlgebraicTopology/SimplicialObject/Op.lean
Modified
Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Op.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/FiniteProd.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Homology/Nondegenerate.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/HornColimits.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesColimit.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/NonsingularColimit.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/PushoutProduct.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/RelativeMorphism.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Skeleton.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexColimits.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Subdivision.lean
Modified
Mathlib/AlgebraicTopology/SingularHomology/Basic.lean
Modified
Mathlib/AlgebraicTopology/SingularSet.lean
Modified
Mathlib/Analysis/Analytic/Composition.lean
Modified
Mathlib/Analysis/Analytic/Inverse.lean
Modified
Mathlib/Analysis/Analytic/IteratedFDeriv.lean
Modified
Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean
Modified
Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
Modified
Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
Modified
Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
Modified
Mathlib/Analysis/BoxIntegral/Partition/Split.lean
Modified
Mathlib/Analysis/BoxIntegral/UnitPartition.lean
Modified
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
Modified
Mathlib/Analysis/CStarAlgebra/Matrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
Modified
Mathlib/Analysis/CStarAlgebra/Spectrum.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitary/Maps.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitization.lean
Modified
Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Analysis/Calculus/Deriv/AffineMap.lean
Modified
Mathlib/Analysis/Calculus/Deriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/Deriv/MeanValue.lean
Modified
Mathlib/Analysis/Calculus/Deriv/Star.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
Modified
Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
Modified
Mathlib/Analysis/Calculus/Implicit.lean
Modified
Mathlib/Analysis/Calculus/MeanValue.lean
Modified
Mathlib/Analysis/Complex/AbsMax.lean
Modified
Mathlib/Analysis/Complex/Circle.lean
Modified
Mathlib/Analysis/Complex/CoveringMap.lean
Modified
Mathlib/Analysis/Complex/Exponential.lean
Modified
Mathlib/Analysis/Complex/Hadamard.lean
Modified
Mathlib/Analysis/Complex/Isometry.lean
Modified
Mathlib/Analysis/Complex/JensenFormula.lean
Modified
Mathlib/Analysis/Complex/Norm.lean
Modified
Mathlib/Analysis/Complex/OpenMapping.lean
Modified
Mathlib/Analysis/Complex/Schwarz.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/ProperAction.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean
Modified
Mathlib/Analysis/Convex/Basic.lean
Modified
Mathlib/Analysis/Convex/Between.lean
Modified
Mathlib/Analysis/Convex/BetweenList.lean
Modified
Mathlib/Analysis/Convex/Birkhoff.lean
Modified
Mathlib/Analysis/Convex/Cone/Extension.lean
Modified
Mathlib/Analysis/Convex/Cone/TensorProduct.lean
Modified
Mathlib/Analysis/Convex/Hull.lean
Modified
Mathlib/Analysis/Convex/Independent.lean
Modified
Mathlib/Analysis/Convex/Intrinsic.lean
Modified
Mathlib/Analysis/Convex/NNReal.lean
Modified
Mathlib/Analysis/Convex/PathConnected.lean
Modified
Mathlib/Analysis/Convex/Segment.lean
Modified
Mathlib/Analysis/Convex/Side.lean
Modified
Mathlib/Analysis/Convex/StrictConvexBetween.lean
Modified
Mathlib/Analysis/Convex/Topology.lean
Modified
Mathlib/Analysis/Convex/Visible.lean
Modified
Mathlib/Analysis/Distribution/TestFunction.lean
Modified
Mathlib/Analysis/Fourier/AddCircle.lean
Modified
Mathlib/Analysis/Fourier/AddCircleMulti.lean
Modified
Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean
Modified
Mathlib/Analysis/Fourier/PoissonSummation.lean
Modified
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
Modified
Mathlib/Analysis/InnerProductSpace/Affine.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Defs.lean
Modified
Mathlib/Analysis/InnerProductSpace/LinearMap.lean
Modified
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
Modified
Mathlib/Analysis/InnerProductSpace/OfNorm.lean
Modified
Mathlib/Analysis/InnerProductSpace/Orientation.lean
Modified
Mathlib/Analysis/InnerProductSpace/PiL2.lean
Modified
Mathlib/Analysis/InnerProductSpace/Positive.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean
Modified
Mathlib/Analysis/InnerProductSpace/Reproducing.lean
Modified
Mathlib/Analysis/InnerProductSpace/Subspace.lean
Modified
Mathlib/Analysis/InnerProductSpace/Symmetric.lean
Modified
Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
Modified
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
Modified
Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean
Modified
Mathlib/Analysis/LocallyConvex/HahnBanach.lean
Modified
Mathlib/Analysis/LocallyConvex/Separation.lean
Modified
Mathlib/Analysis/LocallyConvex/WeakSpace.lean
Modified
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
Modified
Mathlib/Analysis/Matrix/Normed.lean
Modified
Mathlib/Analysis/Matrix/Order.lean
Modified
Mathlib/Analysis/Matrix/PosDef.lean
Modified
Mathlib/Analysis/Matrix/Spectrum.lean
Modified
Mathlib/Analysis/MeanInequalities.lean
Modified
Mathlib/Analysis/Meromorphic/FactorizedRational.lean
Modified
Mathlib/Analysis/Normed/Affine/AddTorsor.lean
Modified
Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean
Modified
Mathlib/Analysis/Normed/Algebra/Exponential.lean
Modified
Mathlib/Analysis/Normed/Algebra/Spectrum.lean
Modified
Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
Modified
Mathlib/Analysis/Normed/Field/Basic.lean
Modified
Mathlib/Analysis/Normed/Field/UnitBall.lean
Modified
Mathlib/Analysis/Normed/Group/AddTorsor.lean
Modified
Mathlib/Analysis/Normed/Group/FunctionSeries.lean
Modified
Mathlib/Analysis/Normed/Group/Quotient.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
Modified
Mathlib/Analysis/Normed/Lp/PiLp.lean
Modified
Mathlib/Analysis/Normed/Lp/ProdLp.lean
Modified
Mathlib/Analysis/Normed/Lp/lpHolder.lean
Modified
Mathlib/Analysis/Normed/Lp/lpSpace.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/Homeomorph.lean
Modified
Mathlib/Analysis/Normed/Module/Bases.lean
Modified
Mathlib/Analysis/Normed/Module/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/ContinuousInverse.lean
Modified
Mathlib/Analysis/Normed/Module/FiniteDimension.lean
Modified
Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/Multilinear/Curry.lean
Modified
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean
Modified
Mathlib/Analysis/Normed/Module/WeakDual.lean
Modified
Mathlib/Analysis/Normed/Operator/Banach.lean
Modified
Mathlib/Analysis/Normed/Operator/Compact/FredholmAlternative.lean
Modified
Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean
Modified
Mathlib/Analysis/Normed/Operator/Extend.lean
Modified
Mathlib/Analysis/Normed/Ring/Basic.lean
Modified
Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
Modified
Mathlib/Analysis/RCLike/Basic.lean
Modified
Mathlib/Analysis/RCLike/BoundedContinuous.lean
Modified
Mathlib/Analysis/RCLike/ContinuousMap.lean
Modified
Mathlib/Analysis/RCLike/Sqrt.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean
Modified
Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean
Modified
Mathlib/Analysis/SpecialFunctions/Sigmoid.lean
Modified
Mathlib/Analysis/SumOverResidueClass.lean
Modified
Mathlib/CategoryTheory/Abelian/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
Modified
Mathlib/CategoryTheory/Abelian/EpiWithInjectiveKernel.lean
Modified
Mathlib/CategoryTheory/Abelian/Ext.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Dimension.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Ext.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
Modified
Mathlib/CategoryTheory/Abelian/LeftDerived.lean
Modified
Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
Modified
Mathlib/CategoryTheory/Abelian/Opposite.lean
Modified
Mathlib/CategoryTheory/Abelian/Preradical/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/Preradical/Colon.lean
Modified
Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
Modified
Mathlib/CategoryTheory/Abelian/Projective/Ext.lean
Modified
Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
Modified
Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
Modified
Mathlib/CategoryTheory/Abelian/RightDerived.lean
Modified
Mathlib/CategoryTheory/Abelian/SerreClass/Localization.lean
Modified
Mathlib/CategoryTheory/Abelian/ShortExact.lean
Modified
Mathlib/CategoryTheory/Abelian/Subobject.lean
Modified
Mathlib/CategoryTheory/Abelian/Transfer.lean
Modified
Mathlib/CategoryTheory/Action.lean
Modified
Mathlib/CategoryTheory/Action/Basic.lean
Modified
Mathlib/CategoryTheory/Action/Concrete.lean
Modified
Mathlib/CategoryTheory/Action/Continuous.lean
Modified
Mathlib/CategoryTheory/Action/Monoidal.lean
Modified
Mathlib/CategoryTheory/Adjunction/Additive.lean
Modified
Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
Modified
Mathlib/CategoryTheory/Adjunction/Basic.lean
Modified
Mathlib/CategoryTheory/Adjunction/CompositionIso.lean
Modified
Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
Modified
Mathlib/CategoryTheory/Adjunction/FullyFaithfulLimits.lean
Modified
Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean
Modified
Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean
Modified
Mathlib/CategoryTheory/Adjunction/Limits.lean
Modified
Mathlib/CategoryTheory/Adjunction/Mates.lean
Modified
Mathlib/CategoryTheory/Adjunction/Opposites.lean
Modified
Mathlib/CategoryTheory/Adjunction/Parametrized.lean
Modified
Mathlib/CategoryTheory/Adjunction/Quadruple.lean
Modified
Mathlib/CategoryTheory/Adjunction/Reflective.lean
Modified
Mathlib/CategoryTheory/Adjunction/Restrict.lean
Modified
Mathlib/CategoryTheory/Adjunction/Triple.lean
Modified
Mathlib/CategoryTheory/Adjunction/Unique.lean
Modified
Mathlib/CategoryTheory/Adjunction/Whiskering.lean
Modified
Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean
Modified
Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
Modified
Mathlib/CategoryTheory/Bicategory/Coherence.lean
Modified
Mathlib/CategoryTheory/Bicategory/Extension.lean
Modified
Mathlib/CategoryTheory/Bicategory/Free.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/Cat/ObjectProperty.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
Modified
Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Pseudo.lean
Modified
Mathlib/CategoryTheory/Bicategory/Grothendieck.lean
Modified
Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean
Modified
Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean
Modified
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean
Modified
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
Modified
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean
Modified
Mathlib/CategoryTheory/Bicategory/Opposites.lean
Modified
Mathlib/CategoryTheory/Bicategory/Product.lean
Modified
Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean
Modified
Mathlib/CategoryTheory/Bicategory/Yoneda.lean
Modified
Mathlib/CategoryTheory/CatCommSq.lean
Modified
Mathlib/CategoryTheory/Category/Bipointed.lean
Modified
Mathlib/CategoryTheory/Category/Cat.lean
Modified
Mathlib/CategoryTheory/Category/Cat/Adjunction.lean
Modified
Mathlib/CategoryTheory/Category/Cat/CartesianClosed.lean
Modified
Mathlib/CategoryTheory/Category/Cat/Limit.lean
Modified
Mathlib/CategoryTheory/Category/Factorisation.lean
Modified
Mathlib/CategoryTheory/Category/KleisliCat.lean
Modified
Mathlib/CategoryTheory/Category/PartialFun.lean
Modified
Mathlib/CategoryTheory/Category/Quiv.lean
Modified
Mathlib/CategoryTheory/Category/ReflQuiv.lean
Modified
Mathlib/CategoryTheory/Category/RelCat.lean
Modified
Mathlib/CategoryTheory/Category/TwoP.lean
Modified
Mathlib/CategoryTheory/Category/ULift.lean
Modified
Mathlib/CategoryTheory/Center/Linear.lean
Modified
Mathlib/CategoryTheory/CofilteredSystem.lean
Modified
Mathlib/CategoryTheory/Comma/Arrow.lean
Modified
Mathlib/CategoryTheory/Comma/Basic.lean
Modified
Mathlib/CategoryTheory/Comma/CardinalArrow.lean
Modified
Mathlib/CategoryTheory/Comma/Final.lean
Modified
Mathlib/CategoryTheory/Comma/Over/Basic.lean
Modified
Mathlib/CategoryTheory/Comma/Over/OverClass.lean
Modified
Mathlib/CategoryTheory/Comma/Over/Pullback.lean
Modified
Mathlib/CategoryTheory/Comma/Over/StrictInitial.lean
Modified
Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
Modified
Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
Modified
Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean
Modified
Mathlib/CategoryTheory/Comma/StructuredArrow/Final.lean
Modified
Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean
Modified
Mathlib/CategoryTheory/ComposableArrows/Basic.lean
Modified
Mathlib/CategoryTheory/ComposableArrows/One.lean
Modified
Mathlib/CategoryTheory/ComposableArrows/Three.lean
Modified
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
Modified
Mathlib/CategoryTheory/ConcreteCategory/Forget.lean
Modified
Mathlib/CategoryTheory/Conj.lean
Modified
Mathlib/CategoryTheory/Core.lean
Modified
Mathlib/CategoryTheory/Dialectica/Monoidal.lean
Modified
Mathlib/CategoryTheory/DifferentialObject.lean
Modified
Mathlib/CategoryTheory/Discrete/Basic.lean
Modified
Mathlib/CategoryTheory/Discrete/StructuredArrow.lean
Modified
Mathlib/CategoryTheory/Discrete/SumsProducts.lean
Modified
Mathlib/CategoryTheory/Distributive/Monoidal.lean
Modified
Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean
Modified
Mathlib/CategoryTheory/EffectiveEpi/Enough.lean
Modified
Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean
Modified
Mathlib/CategoryTheory/Elements.lean
Modified
Mathlib/CategoryTheory/Endofunctor/Algebra.lean
Modified
Mathlib/CategoryTheory/Endomorphism.lean
Modified
Mathlib/CategoryTheory/Enriched/Basic.lean
Modified
Mathlib/CategoryTheory/Enriched/EnrichedCat.lean
Modified
Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
Modified
Mathlib/CategoryTheory/EpiMono.lean
Modified
Mathlib/CategoryTheory/EqToHom.lean
Modified
Mathlib/CategoryTheory/Equivalence.lean
Modified
Mathlib/CategoryTheory/Equivalence/Symmetry.lean
Modified
Mathlib/CategoryTheory/Extensive.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/Fiber.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/Fibered.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean
Modified
Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
Modified
Mathlib/CategoryTheory/Filtered/Final.lean
Modified
Mathlib/CategoryTheory/Filtered/Grothendieck.lean
Modified
Mathlib/CategoryTheory/FinCategory/AsType.lean
Modified
Mathlib/CategoryTheory/FintypeCat.lean
Modified
Mathlib/CategoryTheory/Functor/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/Const.lean
Modified
Mathlib/CategoryTheory/Functor/Currying.lean
Modified
Mathlib/CategoryTheory/Functor/CurryingThree.lean
Modified
Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean
Modified
Mathlib/CategoryTheory/Functor/Derived/PointwiseLeftDerived.lean
Modified
Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean
Modified
Mathlib/CategoryTheory/Functor/EpiMono.lean
Modified
Mathlib/CategoryTheory/Functor/Flat.lean
Modified
Mathlib/CategoryTheory/Functor/FullyFaithful.lean
Modified
Mathlib/CategoryTheory/Functor/FunctorHom.lean
Modified
Mathlib/CategoryTheory/Functor/Functorial.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/DenseAt.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean
Modified
Mathlib/CategoryTheory/Functor/ReflectsIso/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/ReflectsIso/Jointly.lean
Modified
Mathlib/CategoryTheory/Functor/ReflectsIso/Limits.lean
Modified
Mathlib/CategoryTheory/Functor/RegularEpi.lean
Modified
Mathlib/CategoryTheory/Functor/Trifunctor.lean
Modified
Mathlib/CategoryTheory/Functor/TwoSquare.lean
Modified
Mathlib/CategoryTheory/Galois/Action.lean
Modified
Mathlib/CategoryTheory/Galois/Basic.lean
Modified
Mathlib/CategoryTheory/Galois/Decomposition.lean
Modified
Mathlib/CategoryTheory/Galois/Equivalence.lean
Modified
Mathlib/CategoryTheory/Galois/EssSurj.lean
Modified
Mathlib/CategoryTheory/Galois/Examples.lean
Modified
Mathlib/CategoryTheory/Galois/Full.lean
Modified
Mathlib/CategoryTheory/Galois/GaloisObjects.lean
Modified
Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
Modified
Mathlib/CategoryTheory/Galois/Prorepresentability.lean
Modified
Mathlib/CategoryTheory/Galois/Topology.lean
Modified
Mathlib/CategoryTheory/Generator/Basic.lean
Modified
Mathlib/CategoryTheory/Generator/Presheaf.lean
Modified
Mathlib/CategoryTheory/GlueData.lean
Modified
Mathlib/CategoryTheory/GradedObject.lean
Modified
Mathlib/CategoryTheory/GradedObject/Bifunctor.lean
Modified
Mathlib/CategoryTheory/GradedObject/Braiding.lean
Modified
Mathlib/CategoryTheory/GradedObject/Monoidal.lean
Modified
Mathlib/CategoryTheory/GradedObject/Trifunctor.lean
Modified
Mathlib/CategoryTheory/GradedObject/Unitor.lean
Modified
Mathlib/CategoryTheory/Grothendieck.lean
Modified
Mathlib/CategoryTheory/Groupoid.lean
Modified
Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
Modified
Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean
Modified
Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
Modified
Mathlib/CategoryTheory/GuitartExact/Basic.lean
Modified
Mathlib/CategoryTheory/GuitartExact/HorizontalComposition.lean
Modified
Mathlib/CategoryTheory/GuitartExact/KanExtension.lean
Modified
Mathlib/CategoryTheory/GuitartExact/Quotient.lean
Modified
Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
Modified
Mathlib/CategoryTheory/Idempotents/Basic.lean
Modified
Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean
Modified
Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean
Modified
Mathlib/CategoryTheory/Idempotents/HomologicalComplex.lean
Modified
Mathlib/CategoryTheory/Idempotents/Karoubi.lean
Modified
Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
Modified
Mathlib/CategoryTheory/InducedCategory.lean
Modified
Mathlib/CategoryTheory/IsConnected.lean
Modified
Mathlib/CategoryTheory/IsoCat.lean
Modified
Mathlib/CategoryTheory/Join/Basic.lean
Modified
Mathlib/CategoryTheory/Join/Final.lean
Modified
Mathlib/CategoryTheory/Join/Opposites.lean
Modified
Mathlib/CategoryTheory/Join/Pseudofunctor.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/Over.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/PushoutProduct.lean
Modified
Mathlib/CategoryTheory/Limits/Chosen/End.lean
Modified
Mathlib/CategoryTheory/Limits/ColimitLimit.lean
Modified
Mathlib/CategoryTheory/Limits/Comma.lean
Modified
Mathlib/CategoryTheory/Limits/ConeCategory.lean
Modified
Mathlib/CategoryTheory/Limits/Cones.lean
added
theorem
CategoryTheory.Limits.Cocone.w_apply.{uF,
Modified
Mathlib/CategoryTheory/Limits/Connected.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
Modified
Mathlib/CategoryTheory/Limits/Creates.lean
Modified
Mathlib/CategoryTheory/Limits/Elements.lean
Modified
Mathlib/CategoryTheory/Limits/ExactFunctor.lean
Modified
Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
Modified
Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/FintypeCat.lean
Modified
Mathlib/CategoryTheory/Limits/FormalCoproducts/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/FormalCoproducts/ExtraDegeneracy.lean
Modified
Mathlib/CategoryTheory/Limits/Fubini.lean
Modified
Mathlib/CategoryTheory/Limits/FullSubcategory.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/BinaryBiproducts.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/EpiMono.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Images.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/HasLimits.lean
Modified
Mathlib/CategoryTheory/Limits/IndYoneda.lean
Modified
Mathlib/CategoryTheory/Limits/Indization/Category.lean
Modified
Mathlib/CategoryTheory/Limits/Indization/FilteredColimits.lean
Modified
Mathlib/CategoryTheory/Limits/Indization/IndObject.lean
Modified
Mathlib/CategoryTheory/Limits/Indization/LocallySmall.lean
Modified
Mathlib/CategoryTheory/Limits/Indization/ParallelPair.lean
Modified
Mathlib/CategoryTheory/Limits/IsLimit.lean
Modified
Mathlib/CategoryTheory/Limits/MonoCoprod.lean
Modified
Mathlib/CategoryTheory/Limits/MorphismProperty.lean
Modified
Mathlib/CategoryTheory/Limits/Over.lean
Modified
Mathlib/CategoryTheory/Limits/Preorder.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/BifunctorCokernel.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Creates/Opposites.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Grothendieck.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Over.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Over.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Square.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/SigmaConst.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
Modified
Mathlib/CategoryTheory/Limits/Presheaf.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/End.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/FiniteMultiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Images.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Preorder/TransfiniteCompositionOfShape.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/EquifiberedLimits.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackObjObj.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Modified
Mathlib/CategoryTheory/Limits/Sifted.lean
Modified
Mathlib/CategoryTheory/Limits/Types/ColimitType.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Filtered.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Limits.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Multicoequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Yoneda.lean
Modified
Mathlib/CategoryTheory/Limits/VanKampen.lean
Modified
Mathlib/CategoryTheory/Limits/Weighted/HasWeightedLimit.lean
Modified
Mathlib/CategoryTheory/Limits/Yoneda.lean
Modified
Mathlib/CategoryTheory/Localization/Adjunction.lean
Modified
Mathlib/CategoryTheory/Localization/Bifunctor.lean
Modified
Mathlib/CategoryTheory/Localization/Bousfield.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions/OfAdjunction.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
Modified
Mathlib/CategoryTheory/Localization/Construction.lean
Modified
Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean
Modified
Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean
Modified
Mathlib/CategoryTheory/Localization/DerivabilityStructure/Derives.lean
Modified
Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfFunctorialResolutions.lean
Modified
Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfLocalizedEquivalences.lean
Modified
Mathlib/CategoryTheory/Localization/DerivabilityStructure/PointwiseRightDerived.lean
Modified
Mathlib/CategoryTheory/Localization/FiniteProducts.lean
Modified
Mathlib/CategoryTheory/Localization/HasLocalization.lean
Modified
Mathlib/CategoryTheory/Localization/HomEquiv.lean
Modified
Mathlib/CategoryTheory/Localization/Linear.lean
Modified
Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean
Modified
Mathlib/CategoryTheory/Localization/LocallySmall.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Localization/Predicate.lean
Modified
Mathlib/CategoryTheory/Localization/Prod.lean
Modified
Mathlib/CategoryTheory/Localization/Resolution.lean
Modified
Mathlib/CategoryTheory/Localization/SmallHom.lean
Modified
Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
Modified
Mathlib/CategoryTheory/Localization/Triangulated.lean
Modified
Mathlib/CategoryTheory/Localization/Trifunctor.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/ExponentiableMorphism.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean
Modified
Mathlib/CategoryTheory/LocallyDirected.lean
Modified
Mathlib/CategoryTheory/Monad/Adjunction.lean
Modified
Mathlib/CategoryTheory/Monad/Algebra.lean
Modified
Mathlib/CategoryTheory/Monad/Basic.lean
Modified
Mathlib/CategoryTheory/Monad/Coequalizer.lean
Modified
Mathlib/CategoryTheory/Monad/Comonadicity.lean
Modified
Mathlib/CategoryTheory/Monad/Equalizer.lean
Modified
Mathlib/CategoryTheory/Monad/EquivMon.lean
Modified
Mathlib/CategoryTheory/Monad/Kleisli.lean
Modified
Mathlib/CategoryTheory/Monad/Limits.lean
Modified
Mathlib/CategoryTheory/Monad/Monadicity.lean
Modified
Mathlib/CategoryTheory/Monad/Products.lean
Modified
Mathlib/CategoryTheory/Monoidal/Action/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Action/End.lean
Modified
Mathlib/CategoryTheory/Monoidal/Action/Opposites.lean
Modified
Mathlib/CategoryTheory/Monoidal/Arrow.lean
Modified
Mathlib/CategoryTheory/Monoidal/Bimod.lean
Modified
Mathlib/CategoryTheory/Monoidal/Bimon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Multifunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Cat.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/GrpLimits.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Mon.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean
Modified
Mathlib/CategoryTheory/Monoidal/Category.lean
Modified
Mathlib/CategoryTheory/Monoidal/Center.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Complete.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Groupoid.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Ideal.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Types.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Zero.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommComon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommMon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Comon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Conv.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution/Closed.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution/DayFunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/End.lean
Modified
Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean
Modified
Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
Modified
Mathlib/CategoryTheory/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Grp.lean
Modified
Mathlib/CategoryTheory/Monoidal/Hopf_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
Modified
Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Limits/Colimits.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mod.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mon.lean
Modified
Mathlib/CategoryTheory/Monoidal/Multifunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean
Modified
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
Modified
Mathlib/CategoryTheory/Monoidal/Opposite.lean
Modified
Mathlib/CategoryTheory/Monoidal/Opposite/Mon.lean
Modified
Mathlib/CategoryTheory/Monoidal/PushoutProduct.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
Modified
Mathlib/CategoryTheory/Monoidal/Skeleton.lean
Modified
Mathlib/CategoryTheory/Monoidal/Subcategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Transport.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Basic.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Comma.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Concrete.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Factorization.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Limits.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Local.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Representable.lean
Modified
Mathlib/CategoryTheory/NatTrans.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/Equivalence.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/FiniteProducts.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/Opposite.lean
Modified
Mathlib/CategoryTheory/Opposites.lean
Modified
Mathlib/CategoryTheory/PUnit.lean
Modified
Mathlib/CategoryTheory/PathCategory/Basic.lean
Modified
Mathlib/CategoryTheory/PathCategory/MorphismProperty.lean
Modified
Mathlib/CategoryTheory/Pi/Basic.lean
Modified
Mathlib/CategoryTheory/Pi/Monoidal.lean
Modified
Mathlib/CategoryTheory/Preadditive/Biproducts.lean
Modified
Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
Modified
Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean
Modified
Mathlib/CategoryTheory/Preadditive/Injective/Preserves.lean
Modified
Mathlib/CategoryTheory/Preadditive/LeftExact.lean
Modified
Mathlib/CategoryTheory/Preadditive/Mat.lean
Modified
Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean
Modified
Mathlib/CategoryTheory/Preadditive/Projective/Preserves.lean
Modified
Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean
Modified
Mathlib/CategoryTheory/Preadditive/Schur.lean
Modified
Mathlib/CategoryTheory/Preadditive/Transfer.lean
Modified
Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean
Modified
Mathlib/CategoryTheory/Presentable/Adjunction.lean
Modified
Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
Modified
Mathlib/CategoryTheory/Presentable/Dense.lean
Modified
Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
Modified
Mathlib/CategoryTheory/Presentable/Type.lean
Modified
Mathlib/CategoryTheory/Products/Associator.lean
Modified
Mathlib/CategoryTheory/Products/Basic.lean
Modified
Mathlib/CategoryTheory/Products/Bifunctor.lean
Modified
Mathlib/CategoryTheory/Products/Unitor.lean
Modified
Mathlib/CategoryTheory/Quotient.lean
Modified
Mathlib/CategoryTheory/Quotient/Linear.lean
Modified
Mathlib/CategoryTheory/Quotient/Preadditive.lean
Modified
Mathlib/CategoryTheory/Retract.lean
Modified
Mathlib/CategoryTheory/Shift/Adjunction.lean
Modified
Mathlib/CategoryTheory/Shift/Basic.lean
Modified
Mathlib/CategoryTheory/Shift/CommShift.lean
Modified
Mathlib/CategoryTheory/Shift/CommShiftTwo.lean
Modified
Mathlib/CategoryTheory/Shift/Induced.lean
Modified
Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean
Modified
Mathlib/CategoryTheory/Shift/Localization.lean
Modified
Mathlib/CategoryTheory/Shift/Opposite.lean
Modified
Mathlib/CategoryTheory/Shift/Pullback.lean
Modified
Mathlib/CategoryTheory/Shift/ShiftSequence.lean
Modified
Mathlib/CategoryTheory/Shift/ShiftedHom.lean
Modified
Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
Modified
Mathlib/CategoryTheory/Shift/SingleFunctors.lean
Modified
Mathlib/CategoryTheory/Shift/SingleFunctorsLift.lean
Modified
Mathlib/CategoryTheory/ShrinkYoneda.lean
Modified
Mathlib/CategoryTheory/Sigma/Basic.lean
Modified
Mathlib/CategoryTheory/SingleObj.lean
Modified
Mathlib/CategoryTheory/Sites/Adjunction.lean
Modified
Mathlib/CategoryTheory/Sites/Canonical.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
Modified
Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
Modified
Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean
Modified
Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
Modified
Mathlib/CategoryTheory/Sites/ConstantSheaf.lean
Modified
Mathlib/CategoryTheory/Sites/Continuous.lean
Modified
Mathlib/CategoryTheory/Sites/CoverLifting.lean
Modified
Mathlib/CategoryTheory/Sites/CoverPreserving.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.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/Descent/DescentDataPrime.lean
Modified
Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean
Modified
Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean
Modified
Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
Modified
Mathlib/CategoryTheory/Sites/EpiMono.lean
Modified
Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
Modified
Mathlib/CategoryTheory/Sites/Equivalence.lean
Modified
Mathlib/CategoryTheory/Sites/GlobalSections.lean
Modified
Mathlib/CategoryTheory/Sites/Grothendieck.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/Homotopy.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/IsSheaf.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/One.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/Saturate.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean
Modified
Mathlib/CategoryTheory/Sites/IsSheafFor.lean
Modified
Mathlib/CategoryTheory/Sites/Limits.lean
Modified
Mathlib/CategoryTheory/Sites/LocalSite.lean
Modified
Mathlib/CategoryTheory/Sites/Monoidal.lean
Modified
Mathlib/CategoryTheory/Sites/Over.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Comap.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Conservative.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Map.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Monoidal.lean
Modified
Mathlib/CategoryTheory/Sites/Point/OfIsCofiltered.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean
Modified
Mathlib/CategoryTheory/Sites/Precoverage.lean
Modified
Mathlib/CategoryTheory/Sites/Preserves.lean
Modified
Mathlib/CategoryTheory/Sites/PreservesLocallyBijective.lean
Modified
Mathlib/CategoryTheory/Sites/PreservesSheafification.lean
Modified
Mathlib/CategoryTheory/Sites/PseudofunctorSheafOver.lean
Modified
Mathlib/CategoryTheory/Sites/Sheaf.lean
Modified
Mathlib/CategoryTheory/Sites/SheafHom.lean
Modified
Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
Modified
Mathlib/CategoryTheory/Sites/Sheafification.lean
Modified
Mathlib/CategoryTheory/Sites/Sieves.lean
Modified
Mathlib/CategoryTheory/Sites/Subcanonical.lean
Modified
Mathlib/CategoryTheory/Sites/Subsheaf.lean
Modified
Mathlib/CategoryTheory/Sites/Whiskering.lean
Modified
Mathlib/CategoryTheory/Skeletal.lean
Modified
Mathlib/CategoryTheory/SmallObject/Construction.lean
Modified
Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
Modified
Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
Modified
Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
Modified
Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
Modified
Mathlib/CategoryTheory/SmallObject/TransfiniteIteration.lean
Modified
Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean
Modified
Mathlib/CategoryTheory/SmallRepresentatives.lean
Modified
Mathlib/CategoryTheory/Square.lean
Modified
Mathlib/CategoryTheory/Subfunctor/Equalizer.lean
Modified
Mathlib/CategoryTheory/Subfunctor/SubmonoidFunctor.lean
Modified
Mathlib/CategoryTheory/Subobject/ArtinianObject.lean
Modified
Mathlib/CategoryTheory/Subobject/Basic.lean
Modified
Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean
Modified
Mathlib/CategoryTheory/Subobject/Comma.lean
Modified
Mathlib/CategoryTheory/Subobject/FactorThru.lean
Modified
Mathlib/CategoryTheory/Subobject/Lattice.lean
Modified
Mathlib/CategoryTheory/Subobject/Limits.lean
Modified
Mathlib/CategoryTheory/Subobject/MonoOver.lean
Modified
Mathlib/CategoryTheory/Subobject/NoetherianObject.lean
Modified
Mathlib/CategoryTheory/Sums/Associator.lean
Modified
Mathlib/CategoryTheory/Sums/Basic.lean
Modified
Mathlib/CategoryTheory/Sums/Products.lean
Modified
Mathlib/CategoryTheory/Thin.lean
Modified
Mathlib/CategoryTheory/Topos/Sheaf.lean
Modified
Mathlib/CategoryTheory/Triangulated/Adjunction.lean
Modified
Mathlib/CategoryTheory/Triangulated/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/Functor.lean
Modified
Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
Modified
Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean
Modified
Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Subcategory.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/AbelianSubcategory.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/Heart.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/SpectralObject.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/TruncLEGT.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean
Modified
Mathlib/CategoryTheory/Triangulated/TriangleShift.lean
Modified
Mathlib/CategoryTheory/Triangulated/Yoneda.lean
Modified
Mathlib/CategoryTheory/Whiskering.lean
Modified
Mathlib/CategoryTheory/WithTerminal/Basic.lean
Modified
Mathlib/CategoryTheory/WithTerminal/Cone.lean
Modified
Mathlib/CategoryTheory/Yoneda.lean
Modified
Mathlib/Combinatorics/Additive/Corner/Roth.lean
Modified
Mathlib/Combinatorics/Additive/Energy.lean
Modified
Mathlib/Combinatorics/Colex.lean
Modified
Mathlib/Combinatorics/Configuration.lean
Modified
Mathlib/Combinatorics/Derangements/Basic.lean
Modified
Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean
Modified
Mathlib/Combinatorics/Enumerative/Composition.lean
Modified
Mathlib/Combinatorics/Enumerative/DyckWord.lean
Modified
Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
Modified
Mathlib/Combinatorics/Enumerative/Partition/Basic.lean
Modified
Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
Modified
Mathlib/Combinatorics/Hall/Basic.lean
Modified
Mathlib/Combinatorics/Hall/Finite.lean
Modified
Mathlib/Combinatorics/Hindman.lean
Modified
Mathlib/Combinatorics/KatonaCircle.lean
Modified
Mathlib/Combinatorics/Matroid/Basic.lean
Modified
Mathlib/Combinatorics/Matroid/IndepAxioms.lean
Modified
Mathlib/Combinatorics/Matroid/Map.lean
Modified
Mathlib/Combinatorics/Matroid/Sum.lean
Modified
Mathlib/Combinatorics/Quiver/Arborescence.lean
Modified
Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
Modified
Mathlib/Combinatorics/Quiver/Push.lean
Modified
Mathlib/Combinatorics/Quiver/SingleObj.lean
Modified
Mathlib/Combinatorics/Schnirelmann.lean
Modified
Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
Modified
Mathlib/Combinatorics/SetFamily/FourFunctions.lean
Modified
Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Basic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Copy.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Dart.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
Modified
Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
Modified
Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
Modified
Mathlib/Combinatorics/SimpleGraph/LineGraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Maps.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Matching.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Paths.lean
Modified
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Sum.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Trails.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Tutte.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Counting.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean
Modified
Mathlib/Combinatorics/Young/YoungDiagram.lean
Modified
Mathlib/Computability/Ackermann.lean
Modified
Mathlib/Computability/ContextFreeGrammar.lean
Modified
Mathlib/Computability/DFA.lean
Modified
Mathlib/Computability/Encoding.lean
Modified
Mathlib/Computability/Language.lean
Modified
Mathlib/Computability/NFA.lean
Modified
Mathlib/Computability/Partrec.lean
Modified
Mathlib/Computability/PartrecBasis.lean
Modified
Mathlib/Computability/PartrecCode.lean
Modified
Mathlib/Computability/Primrec/Basic.lean
Modified
Mathlib/Computability/Primrec/List.lean
Modified
Mathlib/Computability/RE.lean
Modified
Mathlib/Computability/Reduce.lean
Modified
Mathlib/Computability/TuringMachine/Config.lean
Modified
Mathlib/Computability/TuringMachine/StackTuringMachine.lean
Modified
Mathlib/Computability/TuringMachine/Tape.lean
Modified
Mathlib/Computability/TuringMachine/ToPartrec.lean
Modified
Mathlib/Condensed/Discrete/Colimit.lean
Modified
Mathlib/Condensed/Discrete/LocallyConstant.lean
Modified
Mathlib/Condensed/Light/Functors.lean
Modified
Mathlib/Condensed/Light/InternallyProjective.lean
Modified
Mathlib/Condensed/Light/Small.lean
Modified
Mathlib/Condensed/Light/TopCatAdjunction.lean
Modified
Mathlib/Condensed/TopCatAdjunction.lean
Modified
Mathlib/Control/Applicative.lean
Modified
Mathlib/Control/Bifunctor.lean
Modified
Mathlib/Control/EquivFunctor.lean
Modified
Mathlib/Control/Fold.lean
Modified
Mathlib/Control/Functor.lean
Modified
Mathlib/Control/Functor/Multivariate.lean
Modified
Mathlib/Control/LawfulFix.lean
Modified
Mathlib/Control/Monad/Writer.lean
Modified
Mathlib/Control/Traversable/Equiv.lean
Modified
Mathlib/Control/ULiftable.lean
Modified
Mathlib/Data/Analysis/Filter.lean
Modified
Mathlib/Data/Analysis/Topology.lean
Modified
Mathlib/Data/Complex/Basic.lean
Modified
Mathlib/Data/DFinsupp/BigOperators.lean
Modified
Mathlib/Data/DFinsupp/Defs.lean
Modified
Mathlib/Data/DFinsupp/Lex.lean
Modified
Mathlib/Data/DFinsupp/Multiset.lean
Modified
Mathlib/Data/DFinsupp/WellFounded.lean
Modified
Mathlib/Data/ENNReal/Action.lean
Modified
Mathlib/Data/ENNReal/Inv.lean
Modified
Mathlib/Data/ENNReal/Operations.lean
Modified
Mathlib/Data/EReal/Inv.lean
Modified
Mathlib/Data/EReal/Operations.lean
Modified
Mathlib/Data/Fin/Fin2.lean
Modified
Mathlib/Data/Fin/Tuple/Basic.lean
Modified
Mathlib/Data/Fin/Tuple/Embedding.lean
Modified
Mathlib/Data/Fin/Tuple/Sort.lean
Modified
Mathlib/Data/Fin/Tuple/Take.lean
Modified
Mathlib/Data/FinEnum.lean
Modified
Mathlib/Data/FinEnum/Option.lean
Modified
Mathlib/Data/Finmap.lean
Modified
Mathlib/Data/Finset/Defs.lean
Modified
Mathlib/Data/Finset/Image.lean
Modified
Mathlib/Data/Finset/Insert.lean
Modified
Mathlib/Data/Finset/Lattice/Prod.lean
Modified
Mathlib/Data/Finset/NatAntidiagonal.lean
Modified
Mathlib/Data/Finset/NoncommProd.lean
Modified
Mathlib/Data/Finset/PImage.lean
Modified
Mathlib/Data/Finset/Powerset.lean
Modified
Mathlib/Data/Finset/Preimage.lean
Modified
Mathlib/Data/Finset/Sum.lean
Modified
Mathlib/Data/Finset/Union.lean
Modified
Mathlib/Data/Finsupp/Basic.lean
Modified
Mathlib/Data/Finsupp/Defs.lean
Modified
Mathlib/Data/Finsupp/Lex.lean
Modified
Mathlib/Data/Finsupp/ToDFinsupp.lean
Modified
Mathlib/Data/Finsupp/Weight.lean
Modified
Mathlib/Data/Fintype/Basic.lean
Modified
Mathlib/Data/Fintype/Card.lean
Modified
Mathlib/Data/Fintype/Defs.lean
Modified
Mathlib/Data/Fintype/EquivFin.lean
Modified
Mathlib/Data/Fintype/OfMap.lean
Modified
Mathlib/Data/Fintype/Option.lean
Modified
Mathlib/Data/Fintype/Perm.lean
Modified
Mathlib/Data/Fintype/Quotient.lean
Modified
Mathlib/Data/Fintype/Sets.lean
Modified
Mathlib/Data/Fintype/Sum.lean
Modified
Mathlib/Data/FunLike/Fintype.lean
Modified
Mathlib/Data/Holor.lean
Modified
Mathlib/Data/Int/Cast/Lemmas.lean
Modified
Mathlib/Data/Int/ConditionallyCompleteOrder.lean
Modified
Mathlib/Data/Int/WithZero.lean
Modified
Mathlib/Data/List/Cycle.lean
Modified
Mathlib/Data/List/GetD.lean
Modified
Mathlib/Data/List/NodupEquivFin.lean
Modified
Mathlib/Data/List/Rotate.lean
Modified
Mathlib/Data/Matrix/Basic.lean
Modified
Mathlib/Data/Matrix/Basis.lean
Modified
Mathlib/Data/Matrix/Block.lean
Modified
Mathlib/Data/Matrix/ColumnRowPartitioned.lean
Modified
Mathlib/Data/Matrix/Composition.lean
Modified
Mathlib/Data/Matrix/Mul.lean
Modified
Mathlib/Data/Matrix/PEquiv.lean
Modified
Mathlib/Data/Matrix/Reflection.lean
Modified
Mathlib/Data/Multiset/Bind.lean
Modified
Mathlib/Data/Multiset/Filter.lean
Modified
Mathlib/Data/Multiset/Find.lean
Modified
Mathlib/Data/Multiset/Fintype.lean
Modified
Mathlib/Data/Multiset/Functor.lean
Modified
Mathlib/Data/Multiset/MapFold.lean
Modified
Mathlib/Data/Multiset/Powerset.lean
Modified
Mathlib/Data/NNRat/Defs.lean
Modified
Mathlib/Data/Nat/Cast/Basic.lean
Modified
Mathlib/Data/Nat/Choose/Multinomial.lean
Modified
Mathlib/Data/Nat/Factorization/PrimePow.lean
Modified
Mathlib/Data/Nat/Nth.lean
Modified
Mathlib/Data/Nat/Totient.lean
Modified
Mathlib/Data/Ordmap/Invariants.lean
Modified
Mathlib/Data/Ordmap/Ordset.lean
Modified
Mathlib/Data/PEquiv.lean
Modified
Mathlib/Data/PFun.lean
Modified
Mathlib/Data/PFunctor/Multivariate/Basic.lean
Modified
Mathlib/Data/PFunctor/Multivariate/M.lean
Modified
Mathlib/Data/PFunctor/Multivariate/W.lean
Modified
Mathlib/Data/PFunctor/Univariate/Basic.lean
Modified
Mathlib/Data/PFunctor/Univariate/M.lean
Modified
Mathlib/Data/PNat/Basic.lean
Modified
Mathlib/Data/PNat/Factors.lean
Modified
Mathlib/Data/PNat/Find.lean
Modified
Mathlib/Data/PNat/Interval.lean
Modified
Mathlib/Data/PNat/Prime.lean
Modified
Mathlib/Data/PNat/Xgcd.lean
Modified
Mathlib/Data/Part.lean
Modified
Mathlib/Data/QPF/Multivariate/Basic.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Comp.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Quot.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Sigma.lean
Modified
Mathlib/Data/QPF/Univariate/Basic.lean
Modified
Mathlib/Data/Quot.lean
Modified
Mathlib/Data/Rat/Cast/Defs.lean
Modified
Mathlib/Data/Rat/Cast/Lemmas.lean
Modified
Mathlib/Data/Rat/Cast/OfScientific.lean
Modified
Mathlib/Data/Rat/Lemmas.lean
Modified
Mathlib/Data/Semiquot.lean
Modified
Mathlib/Data/Seq/Basic.lean
modified
theorem
Stream'.Seq.length_nil
Modified
Mathlib/Data/Seq/Defs.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Set/Countable.lean
Modified
Mathlib/Data/Set/Defs.lean
Modified
Mathlib/Data/Set/Finite/Basic.lean
Modified
Mathlib/Data/Set/Finite/Lattice.lean
Modified
Mathlib/Data/Set/Finite/Monad.lean
Modified
Mathlib/Data/Set/NAry.lean
Modified
Mathlib/Data/Set/Operations.lean
Modified
Mathlib/Data/Set/Pairwise/Lattice.lean
Modified
Mathlib/Data/Set/Restrict.lean
Modified
Mathlib/Data/Setoid/Basic.lean
Modified
Mathlib/Data/Setoid/Partition.lean
Modified
Mathlib/Data/Sign/Basic.lean
Modified
Mathlib/Data/Sign/Defs.lean
Modified
Mathlib/Data/String/Basic.lean
Modified
Mathlib/Data/Sum/Basic.lean
Modified
Mathlib/Data/Sym/Basic.lean
Modified
Mathlib/Data/Sym/Sym2.lean
Modified
Mathlib/Data/TypeVec.lean
Modified
Mathlib/Data/Vector/Basic.lean
Modified
Mathlib/Data/Vector/Defs.lean
Modified
Mathlib/Data/W/Basic.lean
Modified
Mathlib/Data/W/Constructions.lean
Modified
Mathlib/Data/WSeq/Basic.lean
Modified
Mathlib/Data/ZMod/Aut.lean
Modified
Mathlib/Data/ZMod/Basic.lean
Modified
Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
Modified
Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
Modified
Mathlib/Dynamics/Ergodic/AddCircle.lean
Modified
Mathlib/Dynamics/Ergodic/Ergodic.lean
Modified
Mathlib/Dynamics/Flow.lean
Modified
Mathlib/FieldTheory/AxGrothendieck.lean
Modified
Mathlib/FieldTheory/CardinalEmb.lean
Modified
Mathlib/FieldTheory/Differential/Basic.lean
Modified
Mathlib/FieldTheory/Extension.lean
Modified
Mathlib/FieldTheory/Finite/Basic.lean
Modified
Mathlib/FieldTheory/Finiteness.lean
Modified
Mathlib/FieldTheory/Fixed.lean
Modified
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
Modified
Mathlib/FieldTheory/Isaacs.lean
Modified
Mathlib/FieldTheory/KrullTopology.lean
Modified
Mathlib/FieldTheory/KummerExtension.lean
Modified
Mathlib/FieldTheory/Minpoly/Field.lean
Modified
Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
Modified
Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
Modified
Mathlib/FieldTheory/Perfect.lean
Modified
Mathlib/FieldTheory/PolynomialGaloisGroup.lean
Modified
Mathlib/FieldTheory/PrimitiveElement.lean
Modified
Mathlib/FieldTheory/PurelyInseparable/Basic.lean
Modified
Mathlib/FieldTheory/RatFunc/Basic.lean
Modified
Mathlib/FieldTheory/RatFunc/IntermediateField.lean
Modified
Mathlib/FieldTheory/RatFunc/Valuation.lean
Modified
Mathlib/FieldTheory/SeparablyGenerated.lean
Modified
Mathlib/Geometry/Convex/Cone/Basic.lean
Modified
Mathlib/Geometry/Convex/Cone/Pointed.lean
Modified
Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean
Modified
Mathlib/Geometry/Convex/ConvexSpace/Defs.lean
Modified
Mathlib/Geometry/Convex/Hull.lean
Modified
Mathlib/Geometry/Convex/Set.lean
Modified
Mathlib/Geometry/Diffeology/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Altitude.lean
Modified
Mathlib/Geometry/Euclidean/Incenter.lean
Modified
Mathlib/Geometry/Euclidean/Inversion/Basic.lean
Modified
Mathlib/Geometry/Euclidean/MongePoint.lean
Modified
Mathlib/Geometry/Euclidean/PerpBisector.lean
Modified
Mathlib/Geometry/Euclidean/SignedDist.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/Tangent.lean
Modified
Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
Modified
Mathlib/Geometry/Manifold/ChartedSpace.lean
Modified
Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
Modified
Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
Modified
Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
Modified
Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean
Modified
Mathlib/Geometry/Manifold/GroupLieAlgebra.lean
Modified
Mathlib/Geometry/Manifold/HasGroupoid.lean
Modified
Mathlib/Geometry/Manifold/Immersion.lean
Modified
Mathlib/Geometry/Manifold/Instances/Icc.lean
Modified
Mathlib/Geometry/Manifold/Instances/Real.lean
Modified
Mathlib/Geometry/Manifold/Instances/Sphere.lean
Modified
Mathlib/Geometry/Manifold/IsManifold/Basic.lean
Modified
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
Modified
Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
Modified
Mathlib/Geometry/Manifold/PartitionOfUnity.lean
Modified
Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean
Modified
Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
Modified
Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
Modified
Mathlib/Geometry/Manifold/VectorField/Pullback.lean
Modified
Mathlib/Geometry/RingedSpace/Basic.lean
Modified
Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
Modified
Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
Modified
Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
Modified
Mathlib/Geometry/RingedSpace/OpenImmersion.lean
Modified
Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
Modified
Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
Modified
Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
Modified
Mathlib/Geometry/RingedSpace/SheafedSpace.lean
Modified
Mathlib/Geometry/RingedSpace/Stalks.lean
Modified
Mathlib/GroupTheory/ArchimedeanDensely.lean
Modified
Mathlib/GroupTheory/ClassEquation.lean
Modified
Mathlib/GroupTheory/Complement.lean
Modified
Mathlib/GroupTheory/Congruence/Basic.lean
Modified
Mathlib/GroupTheory/Congruence/Hom.lean
Modified
Mathlib/GroupTheory/CoprodI.lean
Modified
Mathlib/GroupTheory/Coset/Defs.lean
Modified
Mathlib/GroupTheory/Coxeter/Basic.lean
Modified
Mathlib/GroupTheory/Coxeter/Inversion.lean
Modified
Mathlib/GroupTheory/Coxeter/Matrix.lean
Modified
Mathlib/GroupTheory/Divisible.lean
Modified
Mathlib/GroupTheory/DivisibleHull.lean
Modified
Mathlib/GroupTheory/DoubleCoset.lean
Modified
Mathlib/GroupTheory/Exponent.lean
Modified
Mathlib/GroupTheory/FixedPointFree.lean
Modified
Mathlib/GroupTheory/FreeAbelianGroup.lean
Modified
Mathlib/GroupTheory/FreeGroup/Basic.lean
Modified
Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean
Modified
Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
Modified
Mathlib/GroupTheory/GroupAction/CardCommute.lean
Modified
Mathlib/GroupTheory/GroupAction/ConjAct.lean
Modified
Mathlib/GroupTheory/GroupAction/Hom.lean
Modified
Mathlib/GroupTheory/GroupAction/Jordan.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
Modified
Mathlib/GroupTheory/GroupExtension/Basic.lean
Modified
Mathlib/GroupTheory/HNNExtension.lean
Modified
Mathlib/GroupTheory/Index.lean
Modified
Mathlib/GroupTheory/MonoidLocalization/GrothendieckGroup.lean
Modified
Mathlib/GroupTheory/MonoidLocalization/Maps.lean
Modified
Mathlib/GroupTheory/Nilpotent.lean
Modified
Mathlib/GroupTheory/NoncommCoprod.lean
Modified
Mathlib/GroupTheory/NoncommPiCoprod.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/OreLocalization/Basic.lean
Modified
Mathlib/GroupTheory/PGroup.lean
Modified
Mathlib/GroupTheory/Perm/Centralizer.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Factors.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Type.lean
Modified
Mathlib/GroupTheory/Perm/Fin.lean
Modified
Mathlib/GroupTheory/Perm/Finite.lean
Modified
Mathlib/GroupTheory/Perm/Sign.lean
Modified
Mathlib/GroupTheory/Perm/Support.lean
Modified
Mathlib/GroupTheory/PushoutI.lean
Modified
Mathlib/GroupTheory/QuotientGroup/Basic.lean
Modified
Mathlib/GroupTheory/QuotientGroup/Finite.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating/Simple.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic/Basic.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
Modified
Mathlib/GroupTheory/Subgroup/Center.lean
Modified
Mathlib/GroupTheory/Submonoid/Inverses.lean
Modified
Mathlib/GroupTheory/Sylow.lean
Modified
Mathlib/GroupTheory/Torsion.lean
Modified
Mathlib/Lean/PrettyPrinter/Delaborator.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Shift.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Ceva.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Combination.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Independent.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/MidpointZero.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Slope.lean
Modified
Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
Modified
Mathlib/LinearAlgebra/Basis/Basic.lean
Modified
Mathlib/LinearAlgebra/Basis/Bilinear.lean
Modified
Mathlib/LinearAlgebra/Basis/Cardinality.lean
Modified
Mathlib/LinearAlgebra/Basis/Defs.lean
Modified
Mathlib/LinearAlgebra/Basis/Exact.lean
Modified
Mathlib/LinearAlgebra/Basis/Fin.lean
Modified
Mathlib/LinearAlgebra/Basis/SMul.lean
Modified
Mathlib/LinearAlgebra/Basis/Submodule.lean
Modified
Mathlib/LinearAlgebra/Basis/VectorSpace.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/Properties.lean
Modified
Mathlib/LinearAlgebra/BilinearMap.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
Modified
Mathlib/LinearAlgebra/Complex/Module.lean
Modified
Mathlib/LinearAlgebra/Contraction.lean
Modified
Mathlib/LinearAlgebra/CrossProduct.lean
Modified
Mathlib/LinearAlgebra/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/Determinant.lean
Modified
Mathlib/LinearAlgebra/Dimension/Basic.lean
Modified
Mathlib/LinearAlgebra/Dimension/Constructions.lean
Modified
Mathlib/LinearAlgebra/Dimension/Finite.lean
Modified
Mathlib/LinearAlgebra/Dimension/Free.lean
Modified
Mathlib/LinearAlgebra/Dimension/RankNullity.lean
Modified
Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
Modified
Mathlib/LinearAlgebra/Dimension/Torsion/Basic.lean
Modified
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
Modified
Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/Dual/BaseChange.lean
Modified
Mathlib/LinearAlgebra/Dual/Basis.lean
Modified
Mathlib/LinearAlgebra/Dual/Lemmas.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
Modified
Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
Modified
Mathlib/LinearAlgebra/FiniteSpan.lean
Modified
Mathlib/LinearAlgebra/Finsupp/LSum.lean
Modified
Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
Modified
Mathlib/LinearAlgebra/Finsupp/Pi.lean
Modified
Mathlib/LinearAlgebra/Finsupp/Supported.lean
Modified
Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean
Modified
Mathlib/LinearAlgebra/FixedSubmodule.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Basic.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Int.lean
Modified
Mathlib/LinearAlgebra/FreeModule/PID.lean
Modified
Mathlib/LinearAlgebra/FreeProduct/Basic.lean
Modified
Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean
Modified
Mathlib/LinearAlgebra/Isomorphisms.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
Modified
Mathlib/LinearAlgebra/LinearPMap.lean
Modified
Mathlib/LinearAlgebra/Matrix/Basis.lean
Modified
Mathlib/LinearAlgebra/Matrix/Block.lean
Modified
Mathlib/LinearAlgebra/Matrix/Cartan.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
Modified
Mathlib/LinearAlgebra/Matrix/Dual.lean
Modified
Mathlib/LinearAlgebra/Matrix/DualNumber.lean
Modified
Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
Modified
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Projective.lean
Modified
Mathlib/LinearAlgebra/Matrix/Hadamard.lean
Modified
Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean
Modified
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean
Modified
Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
Modified
Mathlib/LinearAlgebra/Matrix/Notation.lean
Modified
Mathlib/LinearAlgebra/Matrix/PosDef.lean
Modified
Mathlib/LinearAlgebra/Matrix/Rank.lean
Modified
Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
Modified
Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
Modified
Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
Modified
Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLin.lean
Modified
Mathlib/LinearAlgebra/Matrix/Transvection.lean
Modified
Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/Orientation.lean
Modified
Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
Modified
Mathlib/LinearAlgebra/Pi.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean
Modified
Mathlib/LinearAlgebra/Prod.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Action.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Basic.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Basis.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Dual.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Signature.lean
Modified
Mathlib/LinearAlgebra/Quotient/Basic.lean
Modified
Mathlib/LinearAlgebra/Ray.lean
Modified
Mathlib/LinearAlgebra/Reflection.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Base.lean
Modified
Mathlib/LinearAlgebra/RootSystem/BaseChange.lean
Modified
Mathlib/LinearAlgebra/RootSystem/BaseExists.lean
Modified
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Defs.lean
modified
def
RootPairing.indexNeg
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean
Modified
Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean
Modified
Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
Modified
Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
Modified
Mathlib/LinearAlgebra/Semisimple.lean
Modified
Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean
Modified
Mathlib/LinearAlgebra/SesquilinearForm/Star.lean
Modified
Mathlib/LinearAlgebra/Span/Defs.lean
Modified
Mathlib/LinearAlgebra/SpecialLinearGroup.lean
Modified
Mathlib/LinearAlgebra/StdBasis.lean
Modified
Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/TensorPower/Basic.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Pi.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Prod.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Tower.lean
Modified
Mathlib/LinearAlgebra/UnitaryGroup.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Denumerable.lean
Modified
Mathlib/Logic/Embedding/Set.lean
Modified
Mathlib/Logic/Encodable/Basic.lean
Modified
Mathlib/Logic/Equiv/Basic.lean
Modified
Mathlib/Logic/Equiv/Defs.lean
Modified
Mathlib/Logic/Equiv/Embedding.lean
Modified
Mathlib/Logic/Equiv/Fin/Basic.lean
Modified
Mathlib/Logic/Equiv/Fintype.lean
Modified
Mathlib/Logic/Equiv/List.lean
Modified
Mathlib/Logic/Equiv/Option.lean
Modified
Mathlib/Logic/Equiv/PartialEquiv.lean
Modified
Mathlib/Logic/Equiv/Set.lean
Modified
Mathlib/Logic/Relation.lean
Modified
Mathlib/Logic/Small/Defs.lean
Modified
Mathlib/Logic/Unique.lean
Modified
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
Modified
Mathlib/MeasureTheory/Constructions/Cylinders.lean
Modified
Mathlib/MeasureTheory/Constructions/Pi.lean
Modified
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
Modified
Mathlib/MeasureTheory/Constructions/UnitInterval.lean
Modified
Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
Modified
Mathlib/MeasureTheory/Function/AEEqFun.lean
Modified
Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean
Modified
Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
Modified
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFunc.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
Modified
Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
Modified
Mathlib/MeasureTheory/Group/AEStabilizer.lean
Modified
Mathlib/MeasureTheory/Group/Action.lean
Modified
Mathlib/MeasureTheory/Integral/Average.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/L1.lean
Modified
Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean
Modified
Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/DistLEIntegral.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean
Modified
Mathlib/MeasureTheory/Integral/Layercake.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/Pi.lean
Modified
Mathlib/MeasureTheory/Integral/Prod.lean
Modified
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean
Modified
Mathlib/MeasureTheory/Integral/SetToL1.lean
Modified
Mathlib/MeasureTheory/Integral/TorusIntegral.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Invariants.lean
Modified
Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Comap.lean
Modified
Mathlib/MeasureTheory/Measure/Complex.lean
Modified
Mathlib/MeasureTheory/Measure/Content.lean
Modified
Mathlib/MeasureTheory/Measure/ContinuousPreimage.lean
Modified
Mathlib/MeasureTheory/Measure/DiracProba.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Extension.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
Modified
Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean
Modified
Mathlib/MeasureTheory/Measure/Hausdorff.lean
Modified
Mathlib/MeasureTheory/Measure/LevyConvergence.lean
Modified
Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
Modified
Mathlib/MeasureTheory/Measure/Map.lean
Modified
Mathlib/MeasureTheory/Measure/OpenPos.lean
Modified
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Prokhorov.lean
Modified
Mathlib/MeasureTheory/Measure/ResolventTransform.lean
Modified
Mathlib/MeasureTheory/Measure/Restrict.lean
Modified
Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Sub.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/AE.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean
Modified
Mathlib/MeasureTheory/PiSystem.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/AddContent.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/Integral.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/Variation/Semivariation.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/WithDensityVec.lean
Modified
Mathlib/ModelTheory/Algebra/Field/Basic.lean
Modified
Mathlib/ModelTheory/Algebra/Field/CharP.lean
Modified
Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
Modified
Mathlib/ModelTheory/Algebra/Ring/FreeCommRing.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Basic.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean
Modified
Mathlib/ModelTheory/Basic.lean
Modified
Mathlib/ModelTheory/Definability.lean
Modified
Mathlib/ModelTheory/DirectLimit.lean
Modified
Mathlib/ModelTheory/Equivalence.lean
Modified
Mathlib/ModelTheory/FinitelyGenerated.lean
Modified
Mathlib/ModelTheory/Fraisse.lean
Modified
Mathlib/ModelTheory/Graph.lean
Modified
Mathlib/ModelTheory/LanguageMap.lean
Modified
Mathlib/ModelTheory/Order.lean
Modified
Mathlib/ModelTheory/PartialEquiv.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/ModelTheory/Substructures.lean
Modified
Mathlib/ModelTheory/Syntax.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
Modified
Mathlib/NumberTheory/Chebyshev.lean
Modified
Mathlib/NumberTheory/ClassNumber/Finite.lean
Modified
Mathlib/NumberTheory/Dioph.lean
Modified
Mathlib/NumberTheory/Divisors.lean
Modified
Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
Modified
Mathlib/NumberTheory/EulerProduct/ExpLog.lean
Modified
Mathlib/NumberTheory/Height/NumberField.lean
Modified
Mathlib/NumberTheory/KummerDedekind.lean
Modified
Mathlib/NumberTheory/LSeries/Convolution.lean
Modified
Mathlib/NumberTheory/LSeries/Dirichlet.lean
Modified
Mathlib/NumberTheory/LSeries/Injectivity.lean
Modified
Mathlib/NumberTheory/LSeries/Nonvanishing.lean
Modified
Mathlib/NumberTheory/LucasLehmer.lean
Modified
Mathlib/NumberTheory/Modular.lean
Modified
Mathlib/NumberTheory/ModularForms/Bounds.lean
Modified
Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
Modified
Mathlib/NumberTheory/ModularForms/Cusps.lean
Modified
Mathlib/NumberTheory/ModularForms/Discriminant.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean
Modified
Mathlib/NumberTheory/ModularForms/Identities.lean
Modified
Mathlib/NumberTheory/ModularForms/SlashActions.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/Completion/FinitePlace.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Three.lean
Modified
Mathlib/NumberTheory/NumberField/House.lean
Modified
Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean
Modified
Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Norm.lean
Modified
Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
Modified
Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean
Modified
Mathlib/NumberTheory/Padics/Hensel.lean
Modified
Mathlib/NumberTheory/Padics/MahlerBasis.lean
Modified
Mathlib/NumberTheory/Padics/PadicIntegers.lean
Modified
Mathlib/NumberTheory/Padics/RingHoms.lean
Modified
Mathlib/NumberTheory/Padics/WithVal.lean
Modified
Mathlib/NumberTheory/RamificationInertia/Basic.lean
Modified
Mathlib/NumberTheory/RamificationInertia/Ramification.lean
Modified
Mathlib/NumberTheory/SmoothNumbers.lean
Modified
Mathlib/NumberTheory/TsumDivisorsAntidiagonal.lean
Modified
Mathlib/NumberTheory/WellApproximable.lean
Modified
Mathlib/Order/Antisymmetrization.lean
Modified
Mathlib/Order/Atoms.lean
Modified
Mathlib/Order/Birkhoff.lean
Modified
Mathlib/Order/BooleanAlgebra/Defs.lean
Modified
Mathlib/Order/BooleanGenerators.lean
Modified
Mathlib/Order/Bounds/Basic.lean
Modified
Mathlib/Order/BourbakiWitt.lean
Modified
Mathlib/Order/Category/NonemptyFinLinOrd.lean
Modified
Mathlib/Order/Category/PartOrdEmb.lean
Modified
Mathlib/Order/CompactlyGenerated/Intervals.lean
Modified
Mathlib/Order/Comparable.lean
Modified
Mathlib/Order/Compare.lean
Modified
Mathlib/Order/CompleteBooleanAlgebra.lean
Modified
Mathlib/Order/CompleteLattice/Defs.lean
Modified
Mathlib/Order/CompleteLattice/PiLex.lean
Modified
Mathlib/Order/Completion.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
Modified
Mathlib/Order/Copy.lean
Modified
Mathlib/Order/CountableDenseLinearOrder.lean
Modified
Mathlib/Order/Defs/PartialOrder.lean
Modified
Mathlib/Order/DirectedInverseSystem.lean
Modified
Mathlib/Order/Disjointed.lean
Modified
Mathlib/Order/Extension/Well.lean
Modified
Mathlib/Order/Filter/Basic.lean
Modified
Mathlib/Order/Filter/CountableInter.lean
Modified
Mathlib/Order/Filter/Finite.lean
Modified
Mathlib/Order/Filter/Germ/Basic.lean
Modified
Mathlib/Order/Filter/Partial.lean
Modified
Mathlib/Order/Filter/Pointwise.lean
Modified
Mathlib/Order/Filter/Prod.lean
Modified
Mathlib/Order/Filter/Ultrafilter/Basic.lean
Modified
Mathlib/Order/Fin/Tuple.lean
Modified
Mathlib/Order/GaloisConnection/Defs.lean
Modified
Mathlib/Order/Height.lean
Modified
Mathlib/Order/Hom/Basic.lean
Modified
Mathlib/Order/Hom/CompleteLattice.lean
Modified
Mathlib/Order/Hom/Lex.lean
Modified
Mathlib/Order/Hom/PowersetCard.lean
Modified
Mathlib/Order/Hom/Set.lean
Modified
Mathlib/Order/Interval/Finset/Basic.lean
Modified
Mathlib/Order/Interval/Finset/Defs.lean
Modified
Mathlib/Order/Interval/Finset/Fin.lean
Modified
Mathlib/Order/Interval/Finset/Gaps.lean
Modified
Mathlib/Order/Interval/Finset/Nat.lean
Modified
Mathlib/Order/Interval/Set/InitialSeg.lean
Modified
Mathlib/Order/Interval/Set/IsoIoo.lean
Modified
Mathlib/Order/Interval/Set/ProjIcc.lean
Modified
Mathlib/Order/JordanHolder.lean
Modified
Mathlib/Order/KrullDimension.lean
Modified
Mathlib/Order/Lattice.lean
Modified
Mathlib/Order/Lattice/Nat.lean
Modified
Mathlib/Order/LiminfLimsup.lean
Modified
Mathlib/Order/ModularLattice.lean
Modified
Mathlib/Order/Monotone/Basic.lean
Modified
Mathlib/Order/OmegaCompletePartialOrder.lean
Modified
Mathlib/Order/OrderDual.lean
Modified
Mathlib/Order/OrderIsoNat.lean
Modified
Mathlib/Order/PartialSups.lean
Modified
Mathlib/Order/Partition/Finpartition.lean
Modified
Mathlib/Order/PiLex.lean
Modified
Mathlib/Order/RelClasses.lean
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/Order/SetDissipate.lean
Modified
Mathlib/Order/Sublocale.lean
Modified
Mathlib/Order/SuccPred/Basic.lean
Modified
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
Modified
Mathlib/Order/SuccPred/LinearLocallyFinite.lean
Modified
Mathlib/Order/SupClosed.lean
Modified
Mathlib/Order/Types/Defs.lean
Modified
Mathlib/Order/UpperLower/Closure.lean
Modified
Mathlib/Order/UpperLower/CompleteLattice.lean
Modified
Mathlib/Order/WellFounded.lean
Modified
Mathlib/Probability/Distributions/Binomial.lean
Modified
Mathlib/Probability/Distributions/Fernique.lean
Modified
Mathlib/Probability/Distributions/Gaussian/CharFun.lean
Modified
Mathlib/Probability/Distributions/Gaussian/Real.lean
Modified
Mathlib/Probability/Distributions/Uniform.lean
Modified
Mathlib/Probability/Kernel/Composition/CompProd.lean
Modified
Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean
Modified
Mathlib/Probability/Kernel/MeasurableIntegral.lean
Modified
Mathlib/Probability/Martingale/OptionalStopping.lean
Modified
Mathlib/Probability/Moments/ComplexMGF.lean
Modified
Mathlib/Probability/Moments/CovarianceBilin.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Monad.lean
Modified
Mathlib/Probability/Process/Filtration.lean
Modified
Mathlib/Probability/Process/Predictable.lean
Modified
Mathlib/Probability/Process/Stopping.lean
Modified
Mathlib/Probability/ProductMeasure.lean
Modified
Mathlib/RepresentationTheory/Action.lean
Modified
Mathlib/RepresentationTheory/Basic.lean
Modified
Mathlib/RepresentationTheory/Coinduced.lean
Modified
Mathlib/RepresentationTheory/Coinvariants.lean
Modified
Mathlib/RepresentationTheory/Continuous/TopRep.lean
Modified
Mathlib/RepresentationTheory/Equiv.lean
Modified
Mathlib/RepresentationTheory/FDRep.lean
Modified
Mathlib/RepresentationTheory/FiniteIndex.lean
Modified
Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupHomology/LongExactSequence.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
Modified
Mathlib/RepresentationTheory/Homological/Resolution.lean
Modified
Mathlib/RepresentationTheory/Induced.lean
Modified
Mathlib/RepresentationTheory/Intertwining.lean
Modified
Mathlib/RepresentationTheory/Invariants.lean
Modified
Mathlib/RepresentationTheory/Maschke.lean
Modified
Mathlib/RepresentationTheory/Rep/Basic.lean
Modified
Mathlib/RepresentationTheory/Rep/Res.lean
Modified
Mathlib/RepresentationTheory/Submodule.lean
Modified
Mathlib/RepresentationTheory/Tannaka.lean
Modified
Mathlib/RingTheory/AdicCompletion/Algebra.lean
Modified
Mathlib/RingTheory/AdicCompletion/Basic.lean
Modified
Mathlib/RingTheory/AdicCompletion/Completeness.lean
Modified
Mathlib/RingTheory/AdicCompletion/Functoriality.lean
Modified
Mathlib/RingTheory/Adjoin/FG.lean
Modified
Mathlib/RingTheory/Adjoin/PowerBasis.lean
Modified
Mathlib/RingTheory/AdjoinRoot.lean
Modified
Mathlib/RingTheory/AlgebraTower.lean
Modified
Mathlib/RingTheory/Algebraic/Integral.lean
Modified
Mathlib/RingTheory/Algebraic/MvPolynomial.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
Modified
Mathlib/RingTheory/Artinian/Module.lean
Modified
Mathlib/RingTheory/Bezout.lean
Modified
Mathlib/RingTheory/Bialgebra/Basic.lean
Modified
Mathlib/RingTheory/Bialgebra/Equiv.lean
Modified
Mathlib/RingTheory/Bialgebra/Hom.lean
Modified
Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
Modified
Mathlib/RingTheory/ChainOfDivisors.lean
Modified
Mathlib/RingTheory/ClassGroup/Basic.lean
Modified
Mathlib/RingTheory/Coalgebra/Equiv.lean
Modified
Mathlib/RingTheory/Congruence/Hom.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DedekindDomain/Different.lean
Modified
Mathlib/RingTheory/DedekindDomain/Factorization.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
Modified
Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
Modified
Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean
Modified
Mathlib/RingTheory/Derivation/Basic.lean
Modified
Mathlib/RingTheory/Derivation/Lie.lean
Modified
Mathlib/RingTheory/Derivation/MapCoeffs.lean
Modified
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
Modified
Mathlib/RingTheory/DividedPowers/Padic.lean
Modified
Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean
Modified
Mathlib/RingTheory/Etale/Basic.lean
Modified
Mathlib/RingTheory/Etale/Kaehler.lean
Modified
Mathlib/RingTheory/Etale/QuasiFinite.lean
Modified
Mathlib/RingTheory/Etale/StandardEtale.lean
Modified
Mathlib/RingTheory/Etale/Weakly.lean
Modified
Mathlib/RingTheory/EuclideanDomain.lean
Modified
Mathlib/RingTheory/Extension/Basic.lean
Modified
Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean
Modified
Mathlib/RingTheory/Extension/Cotangent/Basic.lean
Modified
Mathlib/RingTheory/Extension/Cotangent/Basis.lean
Modified
Mathlib/RingTheory/Extension/Cotangent/Free.lean
Modified
Mathlib/RingTheory/Extension/Cotangent/LocalizationAway.lean
Modified
Mathlib/RingTheory/Extension/ExtendScalars.lean
Modified
Mathlib/RingTheory/Extension/Generators.lean
Modified
Mathlib/RingTheory/Extension/Presentation/Basic.lean
Modified
Mathlib/RingTheory/Extension/Presentation/Core.lean
Modified
Mathlib/RingTheory/Extension/Presentation/Submersive.lean
Modified
Mathlib/RingTheory/Filtration.lean
Modified
Mathlib/RingTheory/Finiteness/Basic.lean
Modified
Mathlib/RingTheory/Finiteness/FinitePresentationLocal.lean
Modified
Mathlib/RingTheory/Flat/Equalizer.lean
Modified
Mathlib/RingTheory/Flat/Localization.lean
Modified
Mathlib/RingTheory/FormalGroup/Basic.lean
Modified
Mathlib/RingTheory/FractionalIdeal/Basic.lean
Modified
Mathlib/RingTheory/FractionalIdeal/Operations.lean
Modified
Mathlib/RingTheory/FreeCommRing.lean
Modified
Mathlib/RingTheory/Frobenius.lean
Modified
Mathlib/RingTheory/GradedAlgebra/Basic.lean
Modified
Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
Modified
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
Modified
Mathlib/RingTheory/GradedAlgebra/TensorProduct.lean
Modified
Mathlib/RingTheory/HahnSeries/Addition.lean
Modified
Mathlib/RingTheory/HahnSeries/Basic.lean
Modified
Mathlib/RingTheory/HahnSeries/HEval.lean
Modified
Mathlib/RingTheory/HahnSeries/Lex.lean
Modified
Mathlib/RingTheory/HahnSeries/Multiplication.lean
Modified
Mathlib/RingTheory/HahnSeries/Summable.lean
Modified
Mathlib/RingTheory/HopfAlgebra/Basic.lean
Modified
Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
Modified
Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean
Modified
Mathlib/RingTheory/Ideal/Basis.lean
Modified
Mathlib/RingTheory/Ideal/Cotangent.lean
Modified
Mathlib/RingTheory/Ideal/CotangentBaseChange.lean
Modified
Mathlib/RingTheory/Ideal/GoingDown.lean
Modified
Mathlib/RingTheory/Ideal/Height.lean
Modified
Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
Modified
Mathlib/RingTheory/Ideal/Maps.lean
Modified
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/Ideal/Prod.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Basic.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/ChineseRemainder.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Operations.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean
Modified
Mathlib/RingTheory/IdealFilter/Topology.lean
Modified
Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
Modified
Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
Modified
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
Modified
Mathlib/RingTheory/IntegralDomain.lean
Modified
Mathlib/RingTheory/Invariant/Basic.lean
Modified
Mathlib/RingTheory/Invariant/Profinite.lean
Modified
Mathlib/RingTheory/IsAdjoinRoot.lean
Modified
Mathlib/RingTheory/IsPrimary.lean
Modified
Mathlib/RingTheory/IsTensorProduct.lean
Modified
Mathlib/RingTheory/Kaehler/Basic.lean
Modified
Mathlib/RingTheory/Kaehler/JacobiZariski.lean
Modified
Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean
Modified
Mathlib/RingTheory/KrullDimension/Regular.lean
Modified
Mathlib/RingTheory/Lasker.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/LittleWedderburn.lean
Modified
Mathlib/RingTheory/LocalProperties/Basic.lean
Modified
Mathlib/RingTheory/LocalProperties/Projective.lean
Modified
Mathlib/RingTheory/LocalRing/LocalSubring.lean
Modified
Mathlib/RingTheory/LocalRing/Module.lean
Modified
Mathlib/RingTheory/LocalRing/Pullback.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean
Modified
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
Modified
Mathlib/RingTheory/Localization/AtPrime/Extension.lean
Modified
Mathlib/RingTheory/Localization/Away/Basic.lean
Modified
Mathlib/RingTheory/Localization/BaseChange.lean
Modified
Mathlib/RingTheory/Localization/Basic.lean
Modified
Mathlib/RingTheory/Localization/Defs.lean
Modified
Mathlib/RingTheory/Localization/Finiteness.lean
Modified
Mathlib/RingTheory/Localization/FractionRing.lean
Modified
Mathlib/RingTheory/Localization/Ideal.lean
Modified
Mathlib/RingTheory/Localization/Integral.lean
Modified
Mathlib/RingTheory/Localization/LocalizationLocalization.lean
Modified
Mathlib/RingTheory/Localization/Module.lean
Modified
Mathlib/RingTheory/Multiplicity.lean
Modified
Mathlib/RingTheory/MvPolynomial/Expand.lean
Modified
Mathlib/RingTheory/MvPolynomial/Ideal.lean
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
Modified
Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Basic.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Equiv.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Evaluation.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Expand.lean
Modified
Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
Modified
Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Order.lean
Modified
Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Rename.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Substitution.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Trunc.lean
Modified
Mathlib/RingTheory/Nilpotent/Lemmas.lean
Modified
Mathlib/RingTheory/OrderOfVanishing/Basic.lean
Modified
Mathlib/RingTheory/OreLocalization/OreSet.lean
Modified
Mathlib/RingTheory/Perfection.lean
Modified
Mathlib/RingTheory/PiTensorProduct.lean
Modified
Mathlib/RingTheory/PicardGroup.lean
Modified
Mathlib/RingTheory/Polynomial/GaussNorm.lean
Modified
Mathlib/RingTheory/Polynomial/Quotient.lean
Modified
Mathlib/RingTheory/Polynomial/Resultant/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/UniqueFactorization.lean
Modified
Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
Modified
Mathlib/RingTheory/PolynomialLaw/Basic.lean
Modified
Mathlib/RingTheory/PowerBasis.lean
Modified
Mathlib/RingTheory/PowerSeries/Evaluation.lean
Modified
Mathlib/RingTheory/PrincipalIdealDomain.lean
Modified
Mathlib/RingTheory/QuasiFinite/Basic.lean
Modified
Mathlib/RingTheory/QuasiFinite/Polynomial.lean
Modified
Mathlib/RingTheory/QuasiFinite/Weakly.lean
Modified
Mathlib/RingTheory/RamificationInertia/Ramification.lean
Modified
Mathlib/RingTheory/Regular/IsSMulRegular.lean
Modified
Mathlib/RingTheory/Regular/RegularSequence.lean
Modified
Mathlib/RingTheory/RingHom/Locally.lean
Modified
Mathlib/RingTheory/RingHomProperties.lean
Modified
Mathlib/RingTheory/SimpleModule/Basic.lean
Modified
Mathlib/RingTheory/SimpleModule/Isotypic.lean
Modified
Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean
Modified
Mathlib/RingTheory/SimpleRing/Field.lean
Modified
Mathlib/RingTheory/Smooth/AdicCompletion.lean
Modified
Mathlib/RingTheory/Smooth/Basic.lean
Modified
Mathlib/RingTheory/Smooth/IntegralClosure.lean
Modified
Mathlib/RingTheory/Smooth/Kaehler.lean
Modified
Mathlib/RingTheory/Smooth/Pi.lean
Modified
Mathlib/RingTheory/Smooth/Quotient.lean
Modified
Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
Modified
Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean
Modified
Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Basic.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/LTSeries.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
Modified
Mathlib/RingTheory/Support.lean
Modified
Mathlib/RingTheory/TensorProduct/Basic.lean
Modified
Mathlib/RingTheory/TensorProduct/DirectLimitFG.lean
Modified
Mathlib/RingTheory/TensorProduct/Free.lean
Modified
Mathlib/RingTheory/TensorProduct/IsBaseChangeFree.lean
Modified
Mathlib/RingTheory/TensorProduct/Maps.lean
Modified
Mathlib/RingTheory/TensorProduct/Quotient.lean
Modified
Mathlib/RingTheory/TotallySplit.lean
Modified
Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
Modified
Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
Modified
Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/Finite.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/GCDMonoid.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
Modified
Mathlib/RingTheory/Unramified/Basic.lean
Modified
Mathlib/RingTheory/Unramified/LocalStructure.lean
Modified
Mathlib/RingTheory/Valuation/Basic.lean
Modified
Mathlib/RingTheory/Valuation/Discrete/Basic.lean
Modified
Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean
Modified
Mathlib/RingTheory/Valuation/Discrete/RankOne.lean
Modified
Mathlib/RingTheory/Valuation/ExtendToLocalization.lean
Modified
Mathlib/RingTheory/Valuation/Integers.lean
Modified
Mathlib/RingTheory/Valuation/LocalSubring.lean
Modified
Mathlib/RingTheory/Valuation/RankOne.lean
Modified
Mathlib/RingTheory/Valuation/ValuationRing.lean
Modified
Mathlib/RingTheory/Valuation/ValuationSubring.lean
Modified
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
Modified
Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean
Modified
Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
Modified
Mathlib/RingTheory/WittVector/InitTail.lean
Modified
Mathlib/RingTheory/WittVector/Isocrystal.lean
Modified
Mathlib/RingTheory/ZariskisMainTheorem.lean
Modified
Mathlib/SetTheory/Cardinal/Arithmetic.lean
Modified
Mathlib/SetTheory/Cardinal/Basic.lean
Modified
Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
Modified
Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
Modified
Mathlib/SetTheory/Cardinal/Order.lean
Modified
Mathlib/SetTheory/Descriptive/Tree.lean
Modified
Mathlib/SetTheory/Lists.lean
Modified
Mathlib/SetTheory/Ordinal/Arithmetic.lean
Modified
Mathlib/SetTheory/Ordinal/Basic.lean
Modified
Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
Modified
Mathlib/SetTheory/Ordinal/Family.lean
Modified
Mathlib/SetTheory/Ordinal/FundamentalSequence.lean
Modified
Mathlib/SetTheory/ZFC/Basic.lean
Modified
Mathlib/SetTheory/ZFC/Class.lean
Modified
Mathlib/SetTheory/ZFC/Ordinal.lean
Modified
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Basic.lean
Modified
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean
Modified
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean
Modified
Mathlib/Tactic/Core.lean
Modified
Mathlib/Tactic/FieldSimp.lean
Modified
Mathlib/Tactic/FieldSimp/Lemmas.lean
Modified
Mathlib/Tactic/HigherOrder.lean
added
def
Mathlib.Tactic.higherOrderGetParam
added
def
Mathlib.Tactic.mkComp
deleted
def
Tactic.higherOrderGetParam
deleted
def
Tactic.mkComp
Modified
Mathlib/Tactic/Inhabit.lean
Modified
Mathlib/Tactic/Module.lean
Modified
Mathlib/Tactic/NormNum/Basic.lean
Modified
Mathlib/Tactic/NormNum/GCD.lean
added
def
Mathlib.Meta.NormNum.evalIntGCD
added
def
Mathlib.Meta.NormNum.evalIntLCM
added
def
Mathlib.Meta.NormNum.evalNatGCD
added
def
Mathlib.Meta.NormNum.evalNatLCM
added
def
Mathlib.Meta.NormNum.evalRatDen
added
def
Mathlib.Meta.NormNum.evalRatNum
added
theorem
Mathlib.Meta.NormNum.int_gcd_helper'
added
theorem
Mathlib.Meta.NormNum.int_gcd_helper
added
theorem
Mathlib.Meta.NormNum.int_lcm_helper
added
theorem
Mathlib.Meta.NormNum.isInt_gcd
added
theorem
Mathlib.Meta.NormNum.isInt_lcm
added
theorem
Mathlib.Meta.NormNum.isInt_ratNum
added
theorem
Mathlib.Meta.NormNum.isNat_gcd
added
theorem
Mathlib.Meta.NormNum.isNat_lcm
added
theorem
Mathlib.Meta.NormNum.isNat_ratDen
added
theorem
Mathlib.Meta.NormNum.nat_gcd_helper_1'
added
theorem
Mathlib.Meta.NormNum.nat_gcd_helper_1
added
theorem
Mathlib.Meta.NormNum.nat_gcd_helper_2'
added
theorem
Mathlib.Meta.NormNum.nat_gcd_helper_2
added
theorem
Mathlib.Meta.NormNum.nat_gcd_helper_dvd_left
added
theorem
Mathlib.Meta.NormNum.nat_gcd_helper_dvd_right
added
theorem
Mathlib.Meta.NormNum.nat_lcm_helper
added
def
Mathlib.Meta.NormNum.proveIntGCD
added
def
Mathlib.Meta.NormNum.proveIntLCM
added
def
Mathlib.Meta.NormNum.proveNatGCD
added
def
Mathlib.Meta.NormNum.proveNatLCM
deleted
def
Tactic.NormNum.evalIntGCD
deleted
def
Tactic.NormNum.evalIntLCM
deleted
def
Tactic.NormNum.evalNatGCD
deleted
def
Tactic.NormNum.evalNatLCM
deleted
def
Tactic.NormNum.evalRatDen
deleted
def
Tactic.NormNum.evalRatNum
deleted
theorem
Tactic.NormNum.int_gcd_helper'
deleted
theorem
Tactic.NormNum.int_gcd_helper
deleted
theorem
Tactic.NormNum.int_lcm_helper
deleted
theorem
Tactic.NormNum.isInt_gcd
deleted
theorem
Tactic.NormNum.isInt_lcm
deleted
theorem
Tactic.NormNum.isInt_ratNum
deleted
theorem
Tactic.NormNum.isNat_gcd
deleted
theorem
Tactic.NormNum.isNat_lcm
deleted
theorem
Tactic.NormNum.isNat_ratDen
deleted
theorem
Tactic.NormNum.nat_gcd_helper_1'
deleted
theorem
Tactic.NormNum.nat_gcd_helper_1
deleted
theorem
Tactic.NormNum.nat_gcd_helper_2'
deleted
theorem
Tactic.NormNum.nat_gcd_helper_2
deleted
theorem
Tactic.NormNum.nat_gcd_helper_dvd_left
deleted
theorem
Tactic.NormNum.nat_gcd_helper_dvd_right
deleted
theorem
Tactic.NormNum.nat_lcm_helper
deleted
def
Tactic.NormNum.proveIntGCD
deleted
def
Tactic.NormNum.proveIntLCM
deleted
def
Tactic.NormNum.proveNatGCD
deleted
def
Tactic.NormNum.proveNatLCM
Modified
Mathlib/Tactic/NormNum/Irrational.lean
added
structure
Mathlib.Meta.NormNum.NotPowerCertificate
added
def
Mathlib.Meta.NormNum.evalIrrationalRpow
added
def
Mathlib.Meta.NormNum.evalIrrationalSqrt
added
def
Mathlib.Meta.NormNum.findNotPowerCertificate
added
def
Mathlib.Meta.NormNum.findNotPowerCertificateCore
added
theorem
Mathlib.Meta.NormNum.irrational_rpow_nat_rat
added
theorem
Mathlib.Meta.NormNum.irrational_rpow_rat_rat_of_den
added
theorem
Mathlib.Meta.NormNum.irrational_rpow_rat_rat_of_num
added
theorem
Mathlib.Meta.NormNum.irrational_sqrt_nat
added
theorem
Mathlib.Meta.NormNum.irrational_sqrt_rat_of_den
added
theorem
Mathlib.Meta.NormNum.irrational_sqrt_rat_of_num
deleted
structure
Tactic.NormNum.NotPowerCertificate
deleted
def
Tactic.NormNum.evalIrrationalRpow
deleted
def
Tactic.NormNum.evalIrrationalSqrt
deleted
def
Tactic.NormNum.findNotPowerCertificate
deleted
def
Tactic.NormNum.findNotPowerCertificateCore
deleted
theorem
Tactic.NormNum.irrational_rpow_nat_rat
deleted
theorem
Tactic.NormNum.irrational_rpow_rat_rat_of_den
deleted
theorem
Tactic.NormNum.irrational_rpow_rat_rat_of_num
deleted
theorem
Tactic.NormNum.irrational_sqrt_nat
deleted
theorem
Tactic.NormNum.irrational_sqrt_rat_of_den
deleted
theorem
Tactic.NormNum.irrational_sqrt_rat_of_num
Modified
Mathlib/Tactic/NormNum/IsCoprime.lean
added
def
Mathlib.Meta.NormNum.evalIntIsCoprime
added
theorem
Mathlib.Meta.NormNum.int_not_isCoprime_helper
added
theorem
Mathlib.Meta.NormNum.isInt_isCoprime
added
theorem
Mathlib.Meta.NormNum.isInt_not_isCoprime
added
def
Mathlib.Meta.NormNum.proveIntIsCoprime
deleted
def
Tactic.NormNum.evalIntIsCoprime
deleted
theorem
Tactic.NormNum.int_not_isCoprime_helper
deleted
theorem
Tactic.NormNum.isInt_isCoprime
deleted
theorem
Tactic.NormNum.isInt_not_isCoprime
deleted
def
Tactic.NormNum.proveIntIsCoprime
Modified
Mathlib/Tactic/NormNum/IsSquare.lean
Modified
Mathlib/Tactic/NormNum/NatSqrt.lean
added
def
Mathlib.Meta.NormNum.evalNatSqrt
added
theorem
Mathlib.Meta.NormNum.isNat_sqrt
added
theorem
Mathlib.Meta.NormNum.nat_sqrt_helper
added
def
Mathlib.Meta.NormNum.proveNatSqrt
deleted
def
Tactic.NormNum.evalNatSqrt
deleted
theorem
Tactic.NormNum.isNat_sqrt
deleted
theorem
Tactic.NormNum.nat_sqrt_helper
deleted
def
Tactic.NormNum.proveNatSqrt
Modified
Mathlib/Tactic/NormNum/RealSqrt.lean
added
def
Mathlib.Meta.NormNum.evalNNRealSqrt
added
def
Mathlib.Meta.NormNum.evalRealSqrt
added
theorem
Mathlib.Meta.NormNum.isNNRat_nnrealSqrt_of_isNNRat
added
theorem
Mathlib.Meta.NormNum.isNNRat_realSqrt_of_isNNRat
added
theorem
Mathlib.Meta.NormNum.isNat_nnrealSqrt
added
theorem
Mathlib.Meta.NormNum.isNat_realSqrt
added
theorem
Mathlib.Meta.NormNum.isNat_realSqrt_neg
added
theorem
Mathlib.Meta.NormNum.isNat_realSqrt_of_isRat_negOfNat
deleted
def
Tactic.NormNum.evalNNRealSqrt
deleted
def
Tactic.NormNum.evalRealSqrt
deleted
theorem
Tactic.NormNum.isNNRat_nnrealSqrt_of_isNNRat
deleted
theorem
Tactic.NormNum.isNNRat_realSqrt_of_isNNRat
deleted
theorem
Tactic.NormNum.isNat_nnrealSqrt
deleted
theorem
Tactic.NormNum.isNat_realSqrt
deleted
theorem
Tactic.NormNum.isNat_realSqrt_neg
deleted
theorem
Tactic.NormNum.isNat_realSqrt_of_isRat_negOfNat
Modified
Mathlib/Tactic/NormNum/Result.lean
Modified
Mathlib/Tactic/PNatToNat.lean
Modified
Mathlib/Tactic/Ring/RingNF.lean
Modified
Mathlib/Tactic/Simproc/Divisors.lean
Modified
Mathlib/Tactic/Simps/Basic.lean
Modified
Mathlib/Tactic/Translate/Core.lean
Modified
Mathlib/Testing/Plausible/Functions.lean
Modified
Mathlib/Topology/Algebra/Affine.lean
Modified
Mathlib/Topology/Algebra/AffineSubspace.lean
Modified
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Completion.lean
Modified
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
Modified
Mathlib/Topology/Algebra/ContinuousAffineMap.lean
Modified
Mathlib/Topology/Algebra/Field.lean
Modified
Mathlib/Topology/Algebra/FilterBasis.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean
Modified
Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean
Modified
Mathlib/Topology/Algebra/LinearMapCompletion.lean
Modified
Mathlib/Topology/Algebra/LinearTopology.lean
Modified
Mathlib/Topology/Algebra/Module/Complement.lean
Modified
Mathlib/Topology/Algebra/Module/Equiv.lean
Modified
Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
Modified
Mathlib/Topology/Algebra/Module/LinearPMap.lean
Modified
Mathlib/Topology/Algebra/Module/Spaces/CharacterSpace.lean
Modified
Mathlib/Topology/Algebra/Module/Spaces/PointwiseConvergenceCLM.lean
Modified
Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
Modified
Mathlib/Topology/Algebra/Module/Star.lean
Modified
Mathlib/Topology/Algebra/Module/UniformConvergence.lean
Modified
Mathlib/Topology/Algebra/MulAction.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
Modified
Mathlib/Topology/Algebra/RestrictedProduct/Units.lean
Modified
Mathlib/Topology/Algebra/Ring/Compact.lean
Modified
Mathlib/Topology/Algebra/StarSubalgebra.lean
Modified
Mathlib/Topology/Algebra/TopologicallyNilpotent.lean
Modified
Mathlib/Topology/Algebra/UniformFilterBasis.lean
Modified
Mathlib/Topology/Algebra/UniformRing.lean
Modified
Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean
Modified
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
Modified
Mathlib/Topology/Algebra/Valued/NormedValued.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuedField.lean
Modified
Mathlib/Topology/Algebra/Valued/WithVal.lean
Modified
Mathlib/Topology/Basic.lean
Modified
Mathlib/Topology/Bornology/Basic.lean
Modified
Mathlib/Topology/CWComplex/Classical/Basic.lean
Modified
Mathlib/Topology/CWComplex/Classical/Finite.lean
Modified
Mathlib/Topology/Category/CompHausLike/Basic.lean
Modified
Mathlib/Topology/Category/CompHausLike/Cartesian.lean
Modified
Mathlib/Topology/Category/Compactum.lean
Modified
Mathlib/Topology/Category/Profinite/AsLimit.lean
Modified
Mathlib/Topology/Category/Profinite/Nobeling/Basic.lean
Modified
Mathlib/Topology/Category/Profinite/Nobeling/Span.lean
Modified
Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean
Modified
Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean
Modified
Mathlib/Topology/Category/Profinite/Product.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Basic.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Products.lean
Modified
Mathlib/Topology/Category/TopCat/OpenNhds.lean
Modified
Mathlib/Topology/Category/TopCat/Opens.lean
Modified
Mathlib/Topology/Category/TopCat/ULift.lean
Modified
Mathlib/Topology/Category/TopPair.lean
Modified
Mathlib/Topology/Category/UniformSpace.lean
Modified
Mathlib/Topology/CompactOpen.lean
Modified
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
Modified
Mathlib/Topology/Compactification/StoneCech.lean
Modified
Mathlib/Topology/Compactness/Compact.lean
Modified
Mathlib/Topology/Compactness/CompactlyCoherentSpace.lean
Modified
Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
Modified
Mathlib/Topology/Compactness/Lindelof.lean
Modified
Mathlib/Topology/Compactness/LocallyFinite.lean
Modified
Mathlib/Topology/Compactness/SigmaCompact.lean
Modified
Mathlib/Topology/Connected/Clopen.lean
Modified
Mathlib/Topology/Connected/PathConnected.lean
Modified
Mathlib/Topology/Constructible.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/Constructions/SumProd.lean
Modified
Mathlib/Topology/ContinuousMap/Basic.lean
Modified
Mathlib/Topology/ContinuousMap/Compact.lean
Modified
Mathlib/Topology/ContinuousMap/CompactlySupported.lean
Modified
Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
Modified
Mathlib/Topology/ContinuousMap/Sigma.lean
Modified
Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
Modified
Mathlib/Topology/Convenient/GeneratedBy.lean
Modified
Mathlib/Topology/Covering/Basic.lean
Modified
Mathlib/Topology/Covering/Quotient.lean
Modified
Mathlib/Topology/Defs/Filter.lean
Modified
Mathlib/Topology/Defs/Induced.lean
Modified
Mathlib/Topology/EMetricSpace/BoundedVariation.lean
Modified
Mathlib/Topology/EMetricSpace/Defs.lean
Modified
Mathlib/Topology/EMetricSpace/PairReduction.lean
Modified
Mathlib/Topology/FiberBundle/Basic.lean
Modified
Mathlib/Topology/FiberBundle/Constructions.lean
Modified
Mathlib/Topology/FiberBundle/Trivialization.lean
Modified
Mathlib/Topology/FiberPartition.lean
Modified
Mathlib/Topology/Filter.lean
Modified
Mathlib/Topology/Gluing.lean
Modified
Mathlib/Topology/Homeomorph/Lemmas.lean
Modified
Mathlib/Topology/Homotopy/Basic.lean
Modified
Mathlib/Topology/Homotopy/HSpaces.lean
Modified
Mathlib/Topology/Homotopy/HomotopyGroup.lean
Modified
Mathlib/Topology/Homotopy/Lifting.lean
Modified
Mathlib/Topology/Homotopy/Path.lean
Modified
Mathlib/Topology/Homotopy/Product.lean
Modified
Mathlib/Topology/Homotopy/TopCat/Basic.lean
Modified
Mathlib/Topology/Instances/AddCircle/Defs.lean
Modified
Mathlib/Topology/Instances/CantorSet.lean
Modified
Mathlib/Topology/Instances/Complex.lean
Modified
Mathlib/Topology/Instances/ENNReal/Lemmas.lean
Modified
Mathlib/Topology/Irreducible.lean
Modified
Mathlib/Topology/IsClosedRestrict.lean
Modified
Mathlib/Topology/IsLocalHomeomorph.lean
Modified
Mathlib/Topology/MetricSpace/CauSeqFilter.lean
Modified
Mathlib/Topology/MetricSpace/Defs.lean
Modified
Mathlib/Topology/MetricSpace/Gluing.lean
Modified
Mathlib/Topology/MetricSpace/GromovHausdorff.lean
Modified
Mathlib/Topology/MetricSpace/Isometry.lean
Modified
Mathlib/Topology/MetricSpace/PiNat.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
Modified
Mathlib/Topology/Metrizable/CompletelyMetrizable.lean
Modified
Mathlib/Topology/Metrizable/Uniformity.lean
Modified
Mathlib/Topology/Neighborhoods.lean
Modified
Mathlib/Topology/NhdsWithin.lean
Modified
Mathlib/Topology/OmegaCompletePartialOrder.lean
Modified
Mathlib/Topology/Order.lean
Modified
Mathlib/Topology/Order/Basic.lean
Modified
Mathlib/Topology/Order/Bornology.lean
Modified
Mathlib/Topology/Order/Completion.lean
Modified
Mathlib/Topology/Order/HullKernel.lean
Modified
Mathlib/Topology/Order/LawsonTopology.lean
Modified
Mathlib/Topology/Order/LowerUpperTopology.lean
Modified
Mathlib/Topology/Order/ScottTopology.lean
Modified
Mathlib/Topology/Order/UpperLowerSetTopology.lean
Modified
Mathlib/Topology/Order/WithTop.lean
Modified
Mathlib/Topology/Separation/Basic.lean
Modified
Mathlib/Topology/Separation/Hausdorff.lean
Modified
Mathlib/Topology/Sets/Closeds.lean
Modified
Mathlib/Topology/Sets/Opens.lean
Modified
Mathlib/Topology/Sheaves/Alexandrov.lean
Modified
Mathlib/Topology/Sheaves/Flasque.lean
Modified
Mathlib/Topology/Sheaves/Presheaf.lean
Modified
Mathlib/Topology/Sheaves/Skyscraper.lean
Modified
Mathlib/Topology/Sheaves/Stalks.lean
Modified
Mathlib/Topology/Sober.lean
Modified
Mathlib/Topology/Spectral/ConstructibleTopology.lean
Modified
Mathlib/Topology/TietzeExtension.lean
Modified
Mathlib/Topology/UniformSpace/AbsoluteValue.lean
Modified
Mathlib/Topology/UniformSpace/AbstractCompletion.lean
Modified
Mathlib/Topology/UniformSpace/Defs.lean
Modified
Mathlib/Topology/UniformSpace/OfCompactT2.lean
Modified
Mathlib/Topology/UniformSpace/OfFun.lean
Modified
Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
Modified
Mathlib/Topology/UniformSpace/UniformEmbedding.lean
Modified
Mathlib/Topology/UnitInterval.lean
Modified
Mathlib/Topology/VectorBundle/Basic.lean
Modified
Mathlib/Topology/VectorBundle/Constructions.lean
Modified
Mathlib/Util/AddRelatedDecl.lean
added
def
Mathlib.Tactic.warnIfImplicitIllTyped
Modified
Mathlib/Util/CompileInductive.lean
Modified
MathlibTest/CategoryTheory/FunctorAssoc.lean
Modified
MathlibTest/ClickSuggestions/Benchmark.lean
Modified
MathlibTest/DefEqAbuse.lean
Modified
MathlibTest/DeriveFintype.lean
Modified
MathlibTest/FastInstance.lean
Modified
MathlibTest/InferInstanceAsPercent.lean
Modified
MathlibTest/InstanceDiamonds.lean
Modified
MathlibTest/Linter/Whitespace.lean
Modified
MathlibTest/Simproc/VecPerm.lean
Created
MathlibTest/TacticCheckInstancesReassoc.lean
added
def
MyHom
added
theorem
alias_lem2
added
theorem
alias_lem
added
theorem
clean_lem
Created
MathlibTest/TacticCheckInstancesSimps.lean
added
structure
Fn
added
def
MyFn
added
structure
Wrap
added
def
idFn2
added
def
idFn
added
def
mkWrap
Modified
MathlibTest/depRewrite.lean
Modified
MathlibTest/matrix.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
scripts/nolints.json
Modified
scripts/set_option_utils.py