Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-02-17 23:08
33a7291a
View on Github →
chore: bump toolchain to v4.29.0-rc1 (
#35459
)
Estimated changes
Modified
Archive/Examples/Eisenstein.lean
Modified
Archive/Examples/Kuratowski.lean
Modified
Archive/Hairer.lean
Modified
Archive/Imo/Imo1959Q2.lean
Modified
Archive/Imo/Imo1961Q3.lean
Modified
Archive/Imo/Imo1963Q5.lean
Modified
Archive/Imo/Imo1972Q5.lean
Modified
Archive/Imo/Imo1982Q1.lean
Modified
Archive/Imo/Imo1982Q3.lean
Modified
Archive/Imo/Imo1986Q5.lean
Modified
Archive/Imo/Imo1988Q6.lean
Modified
Archive/Imo/Imo1998Q2.lean
Modified
Archive/Imo/Imo2001Q4.lean
Modified
Archive/Imo/Imo2001Q5.lean
Modified
Archive/Imo/Imo2006Q3.lean
Modified
Archive/Imo/Imo2010Q5.lean
Modified
Archive/Imo/Imo2011Q3.lean
Modified
Archive/Imo/Imo2013Q5.lean
Modified
Archive/Imo/Imo2015Q6.lean
Modified
Archive/Imo/Imo2024Q1.lean
Modified
Archive/Imo/Imo2024Q2.lean
Modified
Archive/Imo/Imo2024Q3.lean
Modified
Archive/Imo/Imo2024Q5.lean
Modified
Archive/Imo/Imo2024Q6.lean
Modified
Archive/Kuratowski.lean
Modified
Archive/MiuLanguage/DecisionNec.lean
Modified
Archive/MiuLanguage/DecisionSuf.lean
Modified
Archive/Sensitivity.lean
Modified
Archive/Wiedijk100Theorems/AreaOfACircle.lean
Modified
Archive/Wiedijk100Theorems/BallotProblem.lean
Modified
Archive/Wiedijk100Theorems/BuffonsNeedle.lean
Modified
Archive/Wiedijk100Theorems/CubingACube.lean
modified
theorem
Theorems100.«82».Cube.b_mem_side
Modified
Archive/Wiedijk100Theorems/FriendshipGraphs.lean
Modified
Archive/Wiedijk100Theorems/HeronsFormula.lean
Modified
Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean
Modified
Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean
Modified
Archive/ZagierTwoSquares.lean
Modified
Counterexamples/CliffordAlgebraNotInjective.lean
Modified
Counterexamples/DimensionPolynomial.lean
Modified
Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean
Modified
Counterexamples/HeawoodUnitDistance.lean
Modified
Counterexamples/InvertibleModuleNotIdeal.lean
Modified
Counterexamples/MapFloor.lean
Modified
Counterexamples/NowhereDifferentiable.lean
Modified
Counterexamples/Phillips.lean
Modified
Counterexamples/Pseudoelement.lean
Modified
Counterexamples/SeminormLatticeNotDistrib.lean
Modified
Counterexamples/SorgenfreyLine.lean
Modified
Counterexamples/TopologistsSineCurve.lean
Modified
Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean
Modified
Mathlib/Algebra/AddConstMap/Basic.lean
Modified
Mathlib/Algebra/AffineMonoid/Embedding.lean
Modified
Mathlib/Algebra/AffineMonoid/Irreducible.lean
Modified
Mathlib/Algebra/Algebra/Bilinear.lean
Modified
Mathlib/Algebra/Algebra/Epi.lean
Modified
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Algebra/Operations.lean
deleted
def
Submodule.span.ringHom
deleted
def
Submodule.spanSingleton
Modified
Mathlib/Algebra/Algebra/Opposite.lean
modified
theorem
AlgEquiv.toRingEquiv_opOp
modified
theorem
AlgEquiv.toRingEquiv_toOpposite
Modified
Mathlib/Algebra/Algebra/RestrictScalars.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/IsSimpleOrder.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
Modified
Mathlib/Algebra/Algebra/Unitization.lean
Modified
Mathlib/Algebra/Algebra/ZMod.lean
Modified
Mathlib/Algebra/Azumaya/Matrix.lean
Modified
Mathlib/Algebra/BigOperators/Field.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/Defs.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Indicator.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean
Modified
Mathlib/Algebra/BigOperators/Group/List/Basic.lean
modified
theorem
List.prod_reverse
Modified
Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
Modified
Mathlib/Algebra/BigOperators/Intervals.lean
Modified
Mathlib/Algebra/BigOperators/ModEq.lean
Modified
Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
Modified
Mathlib/Algebra/BigOperators/Ring/Finset.lean
Modified
Mathlib/Algebra/BigOperators/Ring/Nat.lean
Modified
Mathlib/Algebra/Category/AlgCat/Basic.lean
Modified
Mathlib/Algebra/Category/AlgCat/Limits.lean
Modified
Mathlib/Algebra/Category/AlgCat/Symmetric.lean
Modified
Mathlib/Algebra/Category/BialgCat/Basic.lean
Modified
Mathlib/Algebra/Category/BialgCat/Monoidal.lean
Modified
Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean
Modified
Mathlib/Algebra/Category/CommBialgCat.lean
Modified
Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Basic.lean
modified
theorem
LinearMap.comp_id_fgModuleCat
modified
theorem
LinearMap.id_fgModuleCat_comp
Modified
Mathlib/Algebra/Category/FGModuleCat/Colimits.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean
Modified
Mathlib/Algebra/Category/Grp/AB.lean
Modified
Mathlib/Algebra/Category/Grp/Adjunctions.lean
Modified
Mathlib/Algebra/Category/Grp/CartesianMonoidal.lean
Modified
Mathlib/Algebra/Category/Grp/Colimits.lean
Modified
Mathlib/Algebra/Category/Grp/EnoughInjectives.lean
Modified
Mathlib/Algebra/Category/Grp/Kernels.lean
Modified
Mathlib/Algebra/Category/Grp/LargeColimits.lean
Modified
Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
Modified
Mathlib/Algebra/Category/Grp/Limits.lean
Modified
Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean
Modified
Mathlib/Algebra/Category/HopfAlgCat/Monoidal.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Abelian.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Algebra.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Colimits.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/Ext/DimensionShifting.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Ext/Finite.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean
Modified
Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Images.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Kernels.lean
Modified
Mathlib/Algebra/Category/ModuleCat/LeftResolution.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Limits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Localization.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.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/Products.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Projective.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/Abelian.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackContinuous.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/Subobject.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Tannaka.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Ulift.lean
Modified
Mathlib/Algebra/Category/MonCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/MonCat/Colimits.lean
deleted
def
MonCat.Colimits.colimitSetoid
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/Colimits.lean
deleted
def
CommRingCat.Colimits.colimitSetoid
deleted
def
RingCat.Colimits.colimitSetoid
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
Modified
Mathlib/Algebra/Category/Ring/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/Ring/FinitePresentation.lean
Modified
Mathlib/Algebra/Category/Ring/Limits.lean
Modified
Mathlib/Algebra/Category/Ring/LinearAlgebra.lean
Modified
Mathlib/Algebra/Category/Ring/Topology.lean
Modified
Mathlib/Algebra/Category/Ring/Under/Basic.lean
Modified
Mathlib/Algebra/Category/Ring/Under/Limits.lean
Modified
Mathlib/Algebra/Central/End.lean
Modified
Mathlib/Algebra/CharP/Defs.lean
Modified
Mathlib/Algebra/CharP/Invertible.lean
Modified
Mathlib/Algebra/CharP/Lemmas.lean
Modified
Mathlib/Algebra/CharP/LinearMaps.lean
Modified
Mathlib/Algebra/CharP/MixedCharZero.lean
Modified
Mathlib/Algebra/CharP/Quotient.lean
Modified
Mathlib/Algebra/Colimit/DirectLimit.lean
Modified
Mathlib/Algebra/Colimit/Ring.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
Modified
Mathlib/Algebra/DirectSum/Basic.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/DualNumber.lean
Modified
Mathlib/Algebra/DualQuaternion.lean
Modified
Mathlib/Algebra/Exact.lean
Modified
Mathlib/Algebra/Field/Basic.lean
Modified
Mathlib/Algebra/Field/Equiv.lean
Modified
Mathlib/Algebra/Field/Periodic.lean
Modified
Mathlib/Algebra/Field/Power.lean
Modified
Mathlib/Algebra/Field/Subfield/Basic.lean
Modified
Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean
Modified
Mathlib/Algebra/FreeAlgebra.lean
Modified
Mathlib/Algebra/GCDMonoid/Basic.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/AddChar.lean
Modified
Mathlib/Algebra/Group/Conj.lean
Modified
Mathlib/Algebra/Group/Fin/Basic.lean
Modified
Mathlib/Algebra/Group/Finsupp.lean
Modified
Mathlib/Algebra/Group/ForwardDiff.lean
Modified
Mathlib/Algebra/Group/NatPowAssoc.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/Finite.lean
Modified
Mathlib/Algebra/Group/Subgroup/Ker.lean
Modified
Mathlib/Algebra/Group/Subgroup/Lattice.lean
Modified
Mathlib/Algebra/Group/Subgroup/Map.lean
Modified
Mathlib/Algebra/Group/Subgroup/MulOppositeLemmas.lean
Modified
Mathlib/Algebra/Group/Subgroup/Order.lean
Modified
Mathlib/Algebra/Group/Subgroup/Pointwise.lean
Modified
Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
Modified
Mathlib/Algebra/Group/Submonoid/BigOperators.lean
Modified
Mathlib/Algebra/Group/Submonoid/Membership.lean
Modified
Mathlib/Algebra/Group/Submonoid/Pointwise.lean
Modified
Mathlib/Algebra/Group/Submonoid/Units.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean
Modified
Mathlib/Algebra/GroupWithZero/Associated.lean
Modified
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
Modified
Mathlib/Algebra/GroupWithZero/Subgroup.lean
Modified
Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean
Modified
Mathlib/Algebra/Homology/Additive.lean
Modified
Mathlib/Algebra/Homology/AlternatingConst.lean
Modified
Mathlib/Algebra/Homology/Augment.lean
Modified
Mathlib/Algebra/Homology/Bifunctor.lean
Modified
Mathlib/Algebra/Homology/BifunctorAssociator.lean
Modified
Mathlib/Algebra/Homology/BifunctorFlip.lean
Modified
Mathlib/Algebra/Homology/BifunctorHomotopy.lean
Modified
Mathlib/Algebra/Homology/BifunctorShift.lean
Modified
Mathlib/Algebra/Homology/CochainComplexOpposite.lean
Modified
Mathlib/Algebra/Homology/CommSq.lean
Modified
Mathlib/Algebra/Homology/ComplexShapeSigns.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/ExactFunctor.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/TStructure.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/FullyFaithful.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/SingleTriangle.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/SmallShiftedHom.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean
deleted
def
DerivedCategory.TStructure.t
Modified
Mathlib/Algebra/Homology/DifferentialObject.lean
Modified
Mathlib/Algebra/Homology/Double.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/HomEquiv.lean
Modified
Mathlib/Algebra/Homology/Embedding/IsSupported.lean
Modified
Mathlib/Algebra/Homology/Embedding/RestrictionHomology.lean
Modified
Mathlib/Algebra/Homology/Embedding/StupidTrunc.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/Embedding/TruncLEHomology.lean
Modified
Mathlib/Algebra/Homology/EulerCharacteristic.lean
Modified
Mathlib/Algebra/Homology/ExactSequence.lean
Modified
Mathlib/Algebra/Homology/ExactSequenceFour.lean
Modified
Mathlib/Algebra/Homology/Factorizations/CM5b.lean
Modified
Mathlib/Algebra/Homology/Functor.lean
Modified
Mathlib/Algebra/Homology/HomologicalComplex.lean
Modified
Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean
Modified
Mathlib/Algebra/Homology/HomologicalComplexLimits.lean
Modified
Mathlib/Algebra/Homology/HomologySequence.lean
Modified
Mathlib/Algebra/Homology/HomologySequenceLemmas.lean
Modified
Mathlib/Algebra/Homology/Homotopy.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory.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/Pretriangulated.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/SpectralObject.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/Monoidal.lean
Modified
Mathlib/Algebra/Homology/Opposite.lean
Modified
Mathlib/Algebra/Homology/QuasiIso.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Ab.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Abelian.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Exact.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.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/ModuleCat.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Retract.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
Modified
Mathlib/Algebra/Homology/Single.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/BaseChange.lean
Modified
Mathlib/Algebra/Lie/CartanExists.lean
Modified
Mathlib/Algebra/Lie/Classical.lean
Modified
Mathlib/Algebra/Lie/Derivation/Basic.lean
Modified
Mathlib/Algebra/Lie/Derivation/Killing.lean
Modified
Mathlib/Algebra/Lie/DirectSum.lean
Modified
Mathlib/Algebra/Lie/Engel.lean
Modified
Mathlib/Algebra/Lie/EngelSubalgebra.lean
Modified
Mathlib/Algebra/Lie/Extension.lean
Modified
Mathlib/Algebra/Lie/Free.lean
Modified
Mathlib/Algebra/Lie/Ideal.lean
Modified
Mathlib/Algebra/Lie/Killing.lean
Modified
Mathlib/Algebra/Lie/LieTheorem.lean
Modified
Mathlib/Algebra/Lie/Loop.lean
Modified
Mathlib/Algebra/Lie/Nilpotent.lean
Modified
Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean
Modified
Mathlib/Algebra/Lie/Normalizer.lean
Modified
Mathlib/Algebra/Lie/OfAssociative.lean
Modified
Mathlib/Algebra/Lie/Quotient.lean
Modified
Mathlib/Algebra/Lie/Semisimple/Basic.lean
Modified
Mathlib/Algebra/Lie/Semisimple/Lemmas.lean
Modified
Mathlib/Algebra/Lie/SkewAdjoint.lean
Modified
Mathlib/Algebra/Lie/Sl2.lean
Modified
Mathlib/Algebra/Lie/Solvable.lean
Modified
Mathlib/Algebra/Lie/Subalgebra.lean
Modified
Mathlib/Algebra/Lie/Submodule.lean
Modified
Mathlib/Algebra/Lie/TensorProduct.lean
Modified
Mathlib/Algebra/Lie/TraceForm.lean
Modified
Mathlib/Algebra/Lie/UniversalEnveloping.lean
Modified
Mathlib/Algebra/Lie/Weights/Basic.lean
Modified
Mathlib/Algebra/Lie/Weights/Cartan.lean
Modified
Mathlib/Algebra/Lie/Weights/Chain.lean
Modified
Mathlib/Algebra/Lie/Weights/IsSimple.lean
Modified
Mathlib/Algebra/Lie/Weights/Killing.lean
Modified
Mathlib/Algebra/Lie/Weights/Linear.lean
Modified
Mathlib/Algebra/Lie/Weights/RootSystem.lean
Modified
Mathlib/Algebra/LieRinehartAlgebra/Defs.lean
Modified
Mathlib/Algebra/Module/CharacterModule.lean
Modified
Mathlib/Algebra/Module/Congruence/Defs.lean
Modified
Mathlib/Algebra/Module/DedekindDomain.lean
Modified
Mathlib/Algebra/Module/End.lean
Modified
Mathlib/Algebra/Module/Equiv/Basic.lean
Modified
Mathlib/Algebra/Module/FinitePresentation.lean
Modified
Mathlib/Algebra/Module/Hom.lean
Modified
Mathlib/Algebra/Module/Injective.lean
Modified
Mathlib/Algebra/Module/Lattice.lean
Modified
Mathlib/Algebra/Module/LinearMap/Basic.lean
Modified
Mathlib/Algebra/Module/LinearMap/Polynomial.lean
Modified
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
Modified
Mathlib/Algebra/Module/LocalizedModule/Int.lean
Modified
Mathlib/Algebra/Module/NatInt.lean
Modified
Mathlib/Algebra/Module/PID.lean
Modified
Mathlib/Algebra/Module/Presentation/Basic.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/Presentation/Tautological.lean
Modified
Mathlib/Algebra/Module/Presentation/Tensor.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/Pointwise.lean
Modified
Mathlib/Algebra/Module/Submodule/Union.lean
Modified
Mathlib/Algebra/Module/Torsion/Basic.lean
Modified
Mathlib/Algebra/Module/ZLattice/Basic.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/Division.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Grading.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Ideal.lean
Modified
Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Module.lean
Modified
Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Opposite.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Support.lean
Modified
Mathlib/Algebra/MvPolynomial/Basic.lean
Modified
Mathlib/Algebra/MvPolynomial/Degrees.lean
Modified
Mathlib/Algebra/MvPolynomial/Equiv.lean
Modified
Mathlib/Algebra/MvPolynomial/Eval.lean
Modified
Mathlib/Algebra/MvPolynomial/Monad.lean
Modified
Mathlib/Algebra/MvPolynomial/Nilpotent.lean
Modified
Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean
Modified
Mathlib/Algebra/MvPolynomial/PDeriv.lean
Modified
Mathlib/Algebra/MvPolynomial/Rename.lean
Modified
Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean
Modified
Mathlib/Algebra/Notation/Indicator.lean
Modified
Mathlib/Algebra/Notation/Support.lean
Modified
Mathlib/Algebra/Order/AddGroupWithTop.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
deleted
def
FiniteMulArchimedeanClass.subgroup
deleted
def
FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass
Modified
Mathlib/Algebra/Order/CauSeq/BigOperators.lean
Modified
Mathlib/Algebra/Order/Field/Basic.lean
Modified
Mathlib/Algebra/Order/Field/Power.lean
Modified
Mathlib/Algebra/Order/Field/Rat.lean
Modified
Mathlib/Algebra/Order/Floor/Ring.lean
Modified
Mathlib/Algebra/Order/Floor/Semifield.lean
Modified
Mathlib/Algebra/Order/Floor/Semiring.lean
Modified
Mathlib/Algebra/Order/Group/Finset.lean
Modified
Mathlib/Algebra/Order/Group/Int/Sum.lean
Modified
Mathlib/Algebra/Order/Group/PartialSups.lean
Modified
Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Finset.lean
Modified
Mathlib/Algebra/Order/Hom/Monoid.lean
Modified
Mathlib/Algebra/Order/Interval/Basic.lean
Modified
Mathlib/Algebra/Order/Interval/Set/Group.lean
Modified
Mathlib/Algebra/Order/Module/Basic.lean
Modified
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
deleted
def
HahnEmbedding.Partial.toOrderAddMonoidHom
Modified
Mathlib/Algebra/Order/Module/OrderedSMul.lean
Modified
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
Modified
Mathlib/Algebra/Order/Module/Synonym.lean
Modified
Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
Modified
Mathlib/Algebra/Order/Monoid/WithTop.lean
Modified
Mathlib/Algebra/Order/Monovary.lean
Modified
Mathlib/Algebra/Order/Nonneg/Lattice.lean
Modified
Mathlib/Algebra/Order/Nonneg/Ring.lean
Modified
Mathlib/Algebra/Order/Ring/Abs.lean
Modified
Mathlib/Algebra/Order/Ring/Basic.lean
Modified
Mathlib/Algebra/Order/Ring/Cast.lean
Modified
Mathlib/Algebra/Order/Ring/Idempotent.lean
Modified
Mathlib/Algebra/Order/Ring/Int.lean
Modified
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
Modified
Mathlib/Algebra/Order/Ring/Nat.lean
Modified
Mathlib/Algebra/Order/Ring/StandardPart.lean
deleted
def
ArchimedeanClass.FiniteResidueField.mk
deleted
def
ArchimedeanClass.FiniteResidueField.ofArchimedean
Modified
Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
Modified
Mathlib/Algebra/Order/Ring/WithTop.lean
Modified
Mathlib/Algebra/Order/Star/Conjneg.lean
Modified
Mathlib/Algebra/Order/ToIntervalMod.lean
Modified
Mathlib/Algebra/Order/UpperLower.lean
Modified
Mathlib/Algebra/Order/WithTop/Untop0.lean
Modified
Mathlib/Algebra/Pointwise/Stabilizer.lean
Modified
Mathlib/Algebra/Polynomial/AlgebraMap.lean
Modified
Mathlib/Algebra/Polynomial/Basic.lean
Modified
Mathlib/Algebra/Polynomial/BigOperators.lean
Modified
Mathlib/Algebra/Polynomial/Degree/Operations.lean
Modified
Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
Modified
Mathlib/Algebra/Polynomial/Derivative.lean
Modified
Mathlib/Algebra/Polynomial/Div.lean
Modified
Mathlib/Algebra/Polynomial/Expand.lean
Modified
Mathlib/Algebra/Polynomial/FieldDivision.lean
Modified
Mathlib/Algebra/Polynomial/HasseDeriv.lean
Modified
Mathlib/Algebra/Polynomial/Homogenize.lean
Modified
Mathlib/Algebra/Polynomial/Laurent.lean
Modified
Mathlib/Algebra/Polynomial/Mirror.lean
Modified
Mathlib/Algebra/Polynomial/Module/AEval.lean
Modified
Mathlib/Algebra/Polynomial/Module/Basic.lean
Modified
Mathlib/Algebra/Polynomial/Monic.lean
Modified
Mathlib/Algebra/Polynomial/OfFn.lean
Modified
Mathlib/Algebra/Polynomial/Reverse.lean
Modified
Mathlib/Algebra/Polynomial/Roots.lean
Modified
Mathlib/Algebra/Polynomial/Smeval.lean
Modified
Mathlib/Algebra/Polynomial/Splits.lean
Modified
Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
Modified
Mathlib/Algebra/Polynomial/UnitTrinomial.lean
Modified
Mathlib/Algebra/Quandle.lean
Modified
Mathlib/Algebra/Quaternion.lean
Modified
Mathlib/Algebra/Regular/Defs.lean
Modified
Mathlib/Algebra/Ring/BooleanRing.lean
Modified
Mathlib/Algebra/Ring/GeomSum.lean
Modified
Mathlib/Algebra/Ring/Int/Parity.lean
Modified
Mathlib/Algebra/Ring/Invertible.lean
Modified
Mathlib/Algebra/Ring/NegOnePow.lean
Modified
Mathlib/Algebra/Ring/Periodic.lean
Modified
Mathlib/Algebra/Ring/Pointwise/Finset.lean
Modified
Mathlib/Algebra/Ring/Pointwise/Set.lean
Modified
Mathlib/Algebra/Ring/Prod.lean
Modified
Mathlib/Algebra/Ring/Subgroup.lean
Modified
Mathlib/Algebra/Ring/Submonoid/Pointwise.lean
Modified
Mathlib/Algebra/Ring/Subring/Basic.lean
Modified
Mathlib/Algebra/Ring/Subring/MulOpposite.lean
Modified
Mathlib/Algebra/Ring/Subring/Pointwise.lean
Modified
Mathlib/Algebra/Ring/Subsemiring/Basic.lean
Modified
Mathlib/Algebra/Ring/Subsemiring/MulOpposite.lean
Modified
Mathlib/Algebra/Ring/Subsemiring/Pointwise.lean
Modified
Mathlib/Algebra/RingQuot.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Support.lean
Modified
Mathlib/Algebra/SkewPolynomial/Basic.lean
Modified
Mathlib/Algebra/Squarefree/Basic.lean
Modified
Mathlib/Algebra/Star/CentroidHom.lean
Modified
Mathlib/Algebra/Star/LinearMap.lean
Modified
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Star/Pointwise.lean
Modified
Mathlib/Algebra/Star/StarAlgHom.lean
Modified
Mathlib/Algebra/Symmetrized.lean
Modified
Mathlib/Algebra/TrivSqZeroExt.lean
Modified
Mathlib/Algebra/Tropical/Basic.lean
Modified
Mathlib/Algebra/Tropical/BigOperators.lean
Modified
Mathlib/Algebra/Vertex/HVertexOperator.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/ColimitsOver.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/Cover/Sigma.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean
Modified
Mathlib/AlgebraicGeometry/Fiber.lean
Modified
Mathlib/AlgebraicGeometry/FunctionField.lean
Modified
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
Modified
Mathlib/AlgebraicGeometry/Geometrically/Basic.lean
Modified
Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean
Modified
Mathlib/AlgebraicGeometry/Gluing.lean
Modified
Mathlib/AlgebraicGeometry/Group/Abelian.lean
Modified
Mathlib/AlgebraicGeometry/Group/Smooth.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/LimitsOver.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/Finite.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Flat.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/LocalIso.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.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/SchemeTheoreticallyDominant.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean
Modified
Mathlib/AlgebraicGeometry/Noetherian.lean
Modified
Mathlib/AlgebraicGeometry/Normalization.lean
Modified
Mathlib/AlgebraicGeometry/OpenImmersion.lean
Modified
Mathlib/AlgebraicGeometry/PointsPi.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.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/RationalMap.lean
Modified
Mathlib/AlgebraicGeometry/RelativeGluing.lean
Modified
Mathlib/AlgebraicGeometry/Restrict.lean
Modified
Mathlib/AlgebraicGeometry/Scheme.lean
Modified
Mathlib/AlgebraicGeometry/Sites/Etale.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/Decomposition.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Faces.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Projections.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
Modified
Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Basic.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/BifibrantObjectHomotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/BrownLemma.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/CofibrantObjectHomotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Cylinder.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/DerivabilityStructureCofibrant.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/DerivabilityStructureFibrant.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/FibrantObjectHomotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/Homotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/JoyalTrick.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/PathObject.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/RightHomotopy.lean
Modified
Mathlib/AlgebraicTopology/MooreComplex.lean
Modified
Mathlib/AlgebraicTopology/Quasicategory/Basic.lean
Modified
Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean
Modified
Mathlib/AlgebraicTopology/Quasicategory/TwoTruncated.lean
Modified
Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean
Modified
Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.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/Split.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Dimension.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/FiniteColimits.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/FiniteProd.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Horn.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/NonDegenerateSimplices.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Op.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Presentable.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.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/SingularSet.lean
Modified
Mathlib/AlgebraicTopology/TopologicalSimplex.lean
Modified
Mathlib/Analysis/AbsoluteValue/Equivalence.lean
Modified
Mathlib/Analysis/Analytic/Basic.lean
Modified
Mathlib/Analysis/Analytic/Binomial.lean
Modified
Mathlib/Analysis/Analytic/CPolynomial.lean
Modified
Mathlib/Analysis/Analytic/ChangeOrigin.lean
Modified
Mathlib/Analysis/Analytic/Composition.lean
Modified
Mathlib/Analysis/Analytic/Constructions.lean
Modified
Mathlib/Analysis/Analytic/ConvergenceRadius.lean
Modified
Mathlib/Analysis/Analytic/Inverse.lean
Modified
Mathlib/Analysis/Analytic/IteratedFDeriv.lean
Modified
Mathlib/Analysis/Analytic/OfScalars.lean
Modified
Mathlib/Analysis/Analytic/Order.lean
Modified
Mathlib/Analysis/Analytic/Uniqueness.lean
Modified
Mathlib/Analysis/Analytic/Within.lean
Modified
Mathlib/Analysis/Asymptotics/ExpGrowth.lean
Modified
Mathlib/Analysis/Asymptotics/Lemmas.lean
Modified
Mathlib/Analysis/Asymptotics/LinearGrowth.lean
Modified
Mathlib/Analysis/BoundedVariation.lean
Modified
Mathlib/Analysis/BoxIntegral/Basic.lean
Modified
Mathlib/Analysis/BoxIntegral/Box/Basic.lean
Modified
Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
Modified
Mathlib/Analysis/BoxIntegral/Partition/Additive.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/ApproximateUnit.lean
Modified
Mathlib/Analysis/CStarAlgebra/Basic.lean
Modified
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/Classes.lean
Modified
Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Commute.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Continuity.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousMap.lean
Modified
Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
Modified
Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.lean
Modified
Mathlib/Analysis/CStarAlgebra/Hom.lean
Modified
Mathlib/Analysis/CStarAlgebra/Matrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
Modified
Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean
Modified
Mathlib/Analysis/CStarAlgebra/Spectrum.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitary/Span.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitization.lean
Modified
Mathlib/Analysis/CStarAlgebra/lpSpace.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/InnerProduct.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Comp.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Convolution.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Defs.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Operations.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/RestrictScalars.lean
Modified
Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean
Modified
Mathlib/Analysis/Calculus/Deriv/ZPow.lean
Modified
Mathlib/Analysis/Calculus/DerivativeTest.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Congr.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Mul.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Norm.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
Modified
Mathlib/Analysis/Calculus/Implicit.lean
Modified
Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
Modified
Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean
Modified
Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean
Modified
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
Modified
Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
Modified
Mathlib/Analysis/Calculus/LogDeriv.lean
Modified
Mathlib/Analysis/Calculus/MeanValue.lean
Modified
Mathlib/Analysis/Calculus/Monotone.lean
Modified
Mathlib/Analysis/Calculus/Rademacher.lean
Modified
Mathlib/Analysis/Calculus/SmoothSeries.lean
Modified
Mathlib/Analysis/Calculus/TangentCone/Real.lean
Modified
Mathlib/Analysis/Calculus/Taylor.lean
Modified
Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
Modified
Mathlib/Analysis/Calculus/VectorField.lean
Modified
Mathlib/Analysis/Complex/AbelLimit.lean
Modified
Mathlib/Analysis/Complex/AbsMax.lean
Modified
Mathlib/Analysis/Complex/Arg.lean
Modified
Mathlib/Analysis/Complex/Basic.lean
Modified
Mathlib/Analysis/Complex/BorelCaratheodory.lean
Modified
Mathlib/Analysis/Complex/CauchyIntegral.lean
Modified
Mathlib/Analysis/Complex/Circle.lean
Modified
Mathlib/Analysis/Complex/Conformal.lean
Modified
Mathlib/Analysis/Complex/Convex.lean
Modified
Mathlib/Analysis/Complex/CoveringMap.lean
Modified
Mathlib/Analysis/Complex/Exponential.lean
Modified
Mathlib/Analysis/Complex/Hadamard.lean
Modified
Mathlib/Analysis/Complex/Harmonic/Analytic.lean
Modified
Mathlib/Analysis/Complex/Harmonic/MeanValue.lean
Modified
Mathlib/Analysis/Complex/HasPrimitives.lean
Modified
Mathlib/Analysis/Complex/Isometry.lean
Modified
Mathlib/Analysis/Complex/JensenFormula.lean
Modified
Mathlib/Analysis/Complex/LocallyUniformLimit.lean
Modified
Mathlib/Analysis/Complex/MeanValue.lean
Modified
Mathlib/Analysis/Complex/Norm.lean
Modified
Mathlib/Analysis/Complex/OpenMapping.lean
Modified
Mathlib/Analysis/Complex/Order.lean
Modified
Mathlib/Analysis/Complex/Periodic.lean
Modified
Mathlib/Analysis/Complex/PhragmenLindelof.lean
Modified
Mathlib/Analysis/Complex/Polynomial/Basic.lean
Modified
Mathlib/Analysis/Complex/Polynomial/GaussLucas.lean
Modified
Mathlib/Analysis/Complex/RealDeriv.lean
Modified
Mathlib/Analysis/Complex/RemovableSingularity.lean
Modified
Mathlib/Analysis/Complex/Schwarz.lean
Modified
Mathlib/Analysis/Complex/Spectrum.lean
Modified
Mathlib/Analysis/Complex/Tietze.lean
Modified
Mathlib/Analysis/Complex/UnitDisc/Basic.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean
Modified
Mathlib/Analysis/Convex/BetweenList.lean
Modified
Mathlib/Analysis/Convex/Birkhoff.lean
Modified
Mathlib/Analysis/Convex/Body.lean
Modified
Mathlib/Analysis/Convex/Caratheodory.lean
Modified
Mathlib/Analysis/Convex/Combination.lean
Modified
Mathlib/Analysis/Convex/Cone/Basic.lean
Modified
Mathlib/Analysis/Convex/Cone/Dual.lean
Modified
Mathlib/Analysis/Convex/Cone/Extension.lean
Modified
Mathlib/Analysis/Convex/Cone/InnerDual.lean
Modified
Mathlib/Analysis/Convex/Continuous.lean
Modified
Mathlib/Analysis/Convex/Contractible.lean
Modified
Mathlib/Analysis/Convex/Deriv.lean
Modified
Mathlib/Analysis/Convex/EGauge.lean
Modified
Mathlib/Analysis/Convex/Extrema.lean
Modified
Mathlib/Analysis/Convex/Function.lean
Modified
Mathlib/Analysis/Convex/Gauge.lean
Modified
Mathlib/Analysis/Convex/Intrinsic.lean
Modified
Mathlib/Analysis/Convex/Jensen.lean
Modified
Mathlib/Analysis/Convex/NNReal.lean
Modified
Mathlib/Analysis/Convex/Radon.lean
Modified
Mathlib/Analysis/Convex/Segment.lean
Modified
Mathlib/Analysis/Convex/Side.lean
Modified
Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
Modified
Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
Modified
Mathlib/Analysis/Convex/Star.lean
Modified
Mathlib/Analysis/Convex/StoneSeparation.lean
Modified
Mathlib/Analysis/Convex/StrictConvexBetween.lean
Modified
Mathlib/Analysis/Convex/StrictConvexSpace.lean
Modified
Mathlib/Analysis/Convex/Strong.lean
Modified
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean
Modified
Mathlib/Analysis/Distribution/TemperateGrowth.lean
Modified
Mathlib/Analysis/Distribution/TemperedDistribution.lean
Modified
Mathlib/Analysis/Distribution/TestFunction.lean
deleted
def
TestFunction.ofSupportedInCLM
Modified
Mathlib/Analysis/Fourier/AddCircle.lean
Modified
Mathlib/Analysis/Fourier/AddCircleMulti.lean
Modified
Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean
Modified
Mathlib/Analysis/Fourier/Convolution.lean
Modified
Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
Modified
Mathlib/Analysis/Fourier/FourierTransform.lean
Modified
Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
Modified
Mathlib/Analysis/Fourier/Inversion.lean
Modified
Mathlib/Analysis/Fourier/LpSpace.lean
Modified
Mathlib/Analysis/Fourier/PoissonSummation.lean
Modified
Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
Modified
Mathlib/Analysis/Fourier/ZMod.lean
Modified
Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
Modified
Mathlib/Analysis/Hofer.lean
Modified
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Calculus.lean
Modified
Mathlib/Analysis/InnerProductSpace/Coalgebra.lean
Modified
Mathlib/Analysis/InnerProductSpace/Defs.lean
Modified
Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
Modified
Mathlib/Analysis/InnerProductSpace/Harmonic/Constructions.lean
Modified
Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
Modified
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
Modified
Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean
Modified
Mathlib/Analysis/InnerProductSpace/LinearMap.lean
Modified
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
Modified
Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean
Modified
Mathlib/Analysis/InnerProductSpace/NormPow.lean
Modified
Mathlib/Analysis/InnerProductSpace/Orientation.lean
Modified
Mathlib/Analysis/InnerProductSpace/PiL2.lean
Modified
Mathlib/Analysis/InnerProductSpace/Positive.lean
Modified
Mathlib/Analysis/InnerProductSpace/ProdL2.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Minimal.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Reflection.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
Modified
Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
Modified
Mathlib/Analysis/InnerProductSpace/Semisimple.lean
Modified
Mathlib/Analysis/InnerProductSpace/Spectrum.lean
Modified
Mathlib/Analysis/InnerProductSpace/StarOrder.lean
Modified
Mathlib/Analysis/InnerProductSpace/Subspace.lean
Modified
Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
deleted
def
LinearIsometry.lTensor
deleted
def
LinearIsometry.rTensor
deleted
def
LinearIsometryEquiv.lTensor
deleted
def
LinearIsometryEquiv.rTensor
deleted
def
TensorProduct.assocIsometry
deleted
def
TensorProduct.commIsometry
deleted
def
TensorProduct.congrIsometry
deleted
def
TensorProduct.lidIsometry
deleted
def
TensorProduct.mapInclIsometry
deleted
def
TensorProduct.mapIsometry
Modified
Mathlib/Analysis/InnerProductSpace/TwoDim.lean
Modified
Mathlib/Analysis/InnerProductSpace/l2Space.lean
Modified
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
Modified
Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
Modified
Mathlib/Analysis/LocallyConvex/Bounded.lean
Modified
Mathlib/Analysis/LocallyConvex/SeparatingDual.lean
Modified
Mathlib/Analysis/LocallyConvex/WeakDual.lean
Modified
Mathlib/Analysis/LocallyConvex/WeakSpace.lean
Modified
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
Modified
Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean
Modified
Mathlib/Analysis/Matrix/LDL.lean
Modified
Mathlib/Analysis/Matrix/Normed.lean
Modified
Mathlib/Analysis/Matrix/Order.lean
Modified
Mathlib/Analysis/Matrix/Spectrum.lean
Modified
Mathlib/Analysis/MeanInequalities.lean
Modified
Mathlib/Analysis/MellinInversion.lean
Modified
Mathlib/Analysis/MellinTransform.lean
Modified
Mathlib/Analysis/Meromorphic/Divisor.lean
Modified
Mathlib/Analysis/Meromorphic/FactorizedRational.lean
Modified
Mathlib/Analysis/Meromorphic/NormalForm.lean
Modified
Mathlib/Analysis/Meromorphic/Order.lean
Modified
Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean
Modified
Mathlib/Analysis/Normed/Affine/AddTorsor.lean
Modified
Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean
Modified
Mathlib/Analysis/Normed/Affine/Isometry.lean
Modified
Mathlib/Analysis/Normed/Algebra/Basic.lean
Modified
Mathlib/Analysis/Normed/Algebra/DualNumber.lean
Modified
Mathlib/Analysis/Normed/Algebra/Exponential.lean
Modified
Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean
Modified
Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
Modified
Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
Modified
Mathlib/Analysis/Normed/Algebra/Spectrum.lean
Modified
Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
Modified
Mathlib/Analysis/Normed/Algebra/Unitization.lean
Modified
Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean
Modified
Mathlib/Analysis/Normed/Field/Lemmas.lean
Modified
Mathlib/Analysis/Normed/Field/Ultra.lean
Modified
Mathlib/Analysis/Normed/Field/UnitBall.lean
Modified
Mathlib/Analysis/Normed/Field/WithAbs.lean
Modified
Mathlib/Analysis/Normed/Group/AddCircle.lean
Modified
Mathlib/Analysis/Normed/Group/Basic.lean
Modified
Mathlib/Analysis/Normed/Group/Constructions.lean
Modified
Mathlib/Analysis/Normed/Group/Hom.lean
Modified
Mathlib/Analysis/Normed/Group/HomCompletion.lean
Modified
Mathlib/Analysis/Normed/Group/Quotient.lean
Modified
Mathlib/Analysis/Normed/Group/Real.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
Modified
Mathlib/Analysis/Normed/Group/Ultra.lean
Modified
Mathlib/Analysis/Normed/Group/ZeroAtInfty.lean
Modified
Mathlib/Analysis/Normed/Lp/PiLp.lean
Modified
Mathlib/Analysis/Normed/Lp/ProdLp.lean
Modified
Mathlib/Analysis/Normed/Lp/lpSpace.lean
Modified
Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/Action.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/Homeomorph.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/Pointwise.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/RadialEquiv.lean
Modified
Mathlib/Analysis/Normed/Module/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/Complemented.lean
Modified
Mathlib/Analysis/Normed/Module/Connected.lean
Modified
Mathlib/Analysis/Normed/Module/Convex.lean
Modified
Mathlib/Analysis/Normed/Module/Dual.lean
Modified
Mathlib/Analysis/Normed/Module/FiniteDimension.lean
Modified
Mathlib/Analysis/Normed/Module/HahnBanach.lean
Modified
Mathlib/Analysis/Normed/Module/MStructure.lean
Modified
Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean
Modified
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean
Modified
Mathlib/Analysis/Normed/Module/RCLike/Basic.lean
Modified
Mathlib/Analysis/Normed/Module/RCLike/Extend.lean
Modified
Mathlib/Analysis/Normed/Module/RCLike/Real.lean
Modified
Mathlib/Analysis/Normed/Module/Span.lean
Modified
Mathlib/Analysis/Normed/Operator/Banach.lean
Modified
Mathlib/Analysis/Normed/Operator/Basic.lean
Modified
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
Modified
Mathlib/Analysis/Normed/Operator/Extend.lean
Modified
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
Modified
Mathlib/Analysis/Normed/Operator/Mul.lean
Modified
Mathlib/Analysis/Normed/Operator/NNNorm.lean
Modified
Mathlib/Analysis/Normed/Operator/NormedSpace.lean
Modified
Mathlib/Analysis/Normed/Operator/Prod.lean
Modified
Mathlib/Analysis/Normed/Order/Hom/Ultra.lean
Modified
Mathlib/Analysis/Normed/Order/Lattice.lean
Modified
Mathlib/Analysis/Normed/Order/UpperLower.lean
Modified
Mathlib/Analysis/Normed/Ring/Lemmas.lean
Modified
Mathlib/Analysis/Normed/Ring/Ultra.lean
Modified
Mathlib/Analysis/Normed/Ring/Units.lean
Modified
Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean
Modified
Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
Modified
Mathlib/Analysis/Normed/Unbundled/IsPowMulFaithful.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean
Modified
Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
Modified
Mathlib/Analysis/ODE/PicardLindelof.lean
Modified
Mathlib/Analysis/Oscillation.lean
Modified
Mathlib/Analysis/PSeries.lean
Modified
Mathlib/Analysis/Polynomial/CauchyBound.lean
Modified
Mathlib/Analysis/Polynomial/Fourier.lean
Modified
Mathlib/Analysis/Polynomial/MahlerMeasure.lean
Modified
Mathlib/Analysis/Quaternion.lean
deleted
def
Quaternion.ofComplex
Modified
Mathlib/Analysis/RCLike/Basic.lean
deleted
def
RCLike.imLm
deleted
def
RCLike.reLm
Modified
Mathlib/Analysis/RCLike/Inner.lean
Modified
Mathlib/Analysis/RCLike/Sqrt.lean
Modified
Mathlib/Analysis/Real/Cardinality.lean
Modified
Mathlib/Analysis/Real/Hyperreal.lean
Modified
Mathlib/Analysis/Real/OfDigits.lean
Modified
Mathlib/Analysis/Real/Pi/Bounds.lean
Modified
Mathlib/Analysis/Real/Pi/Irrational.lean
Modified
Mathlib/Analysis/Real/Spectrum.lean
Modified
Mathlib/Analysis/Seminorm.lean
Modified
Mathlib/Analysis/SpecialFunctions/ArithmeticGeometricMean.lean
Modified
Mathlib/Analysis/SpecialFunctions/Arsinh.lean
Modified
Mathlib/Analysis/SpecialFunctions/Artanh.lean
Modified
Mathlib/Analysis/SpecialFunctions/Bernstein.lean
Modified
Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
modified
theorem
Complex.arg_I
modified
theorem
Complex.arg_neg_I
modified
theorem
Complex.arg_neg_one
modified
theorem
Complex.arg_zero
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean
Modified
Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean
Modified
Mathlib/Analysis/SpecialFunctions/Exp.lean
Modified
Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
Modified
Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean
Modified
Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Base.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/InvLog.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
Modified
Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
Modified
Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
Modified
Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
Modified
Mathlib/Analysis/SpecialFunctions/Sigmoid.lean
Modified
Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
Modified
Mathlib/Analysis/SpecialFunctions/Stirling.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/DerivHyp.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
Modified
Mathlib/Analysis/SpecificLimits/Basic.lean
Modified
Mathlib/Analysis/SpecificLimits/Fibonacci.lean
Modified
Mathlib/Analysis/SpecificLimits/Normed.lean
Modified
Mathlib/Analysis/SumOverResidueClass.lean
Modified
Mathlib/CategoryTheory/Abelian/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/CommSq.lean
Modified
Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
Modified
Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
Modified
Mathlib/CategoryTheory/Abelian/Exact.lean
Modified
Mathlib/CategoryTheory/Abelian/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/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/GrothendieckCategory/ModuleEmbedding/Opposite.lean
Modified
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
Modified
Mathlib/CategoryTheory/Abelian/Images.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Dimension.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Ext.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Extend.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/Projective/Dimension.lean
Modified
Mathlib/CategoryTheory/Abelian/Projective/Ext.lean
Modified
Mathlib/CategoryTheory/Abelian/Projective/Extend.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/MorphismProperty.lean
Modified
Mathlib/CategoryTheory/Abelian/Transfer.lean
Modified
Mathlib/CategoryTheory/Abelian/Yoneda.lean
Modified
Mathlib/CategoryTheory/Action.lean
Modified
Mathlib/CategoryTheory/Action/Basic.lean
Modified
Mathlib/CategoryTheory/Action/Continuous.lean
Modified
Mathlib/CategoryTheory/Action/Monoidal.lean
Modified
Mathlib/CategoryTheory/Adhesive/Basic.lean
Modified
Mathlib/CategoryTheory/Adjunction/Additive.lean
Modified
Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
Modified
Mathlib/CategoryTheory/Adjunction/Basic.lean
Modified
Mathlib/CategoryTheory/Adjunction/Comma.lean
Modified
Mathlib/CategoryTheory/Adjunction/CompositionIso.lean
Modified
Mathlib/CategoryTheory/Adjunction/Evaluation.lean
Modified
Mathlib/CategoryTheory/Adjunction/FullyFaithful.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/PartialAdjoint.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/Basic.lean
Modified
Mathlib/CategoryTheory/Bicategory/Coherence.lean
Modified
Mathlib/CategoryTheory/Bicategory/Extension.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/Functor/StrictPseudofunctor.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.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/Kan/IsKan.lean
Modified
Mathlib/CategoryTheory/Bicategory/LocallyGroupoid.lean
Modified
Mathlib/CategoryTheory/Bicategory/Modification/Pseudo.lean
Modified
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean
Modified
Mathlib/CategoryTheory/Bicategory/SingleObj.lean
Modified
Mathlib/CategoryTheory/CatCommSq.lean
Modified
Mathlib/CategoryTheory/Category/Basic.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/Cat/Terminal.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/ULift.lean
Modified
Mathlib/CategoryTheory/Center/Linear.lean
Modified
Mathlib/CategoryTheory/Center/Localization.lean
Modified
Mathlib/CategoryTheory/Center/NegOnePow.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/Pullback.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/Four.lean
Modified
Mathlib/CategoryTheory/ComposableArrows/Three.lean
Modified
Mathlib/CategoryTheory/ConnectedComponents.lean
Modified
Mathlib/CategoryTheory/CopyDiscardCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Core.lean
Modified
Mathlib/CategoryTheory/Dialectica/Basic.lean
Modified
Mathlib/CategoryTheory/Dialectica/Monoidal.lean
Modified
Mathlib/CategoryTheory/DifferentialObject.lean
Modified
Mathlib/CategoryTheory/Distributive/Cartesian.lean
Modified
Mathlib/CategoryTheory/Distributive/Monoidal.lean
Modified
Mathlib/CategoryTheory/EffectiveEpi/Basic.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/Enriched/Basic.lean
Modified
Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Enriched/Limits/HasConicalLimits.lean
Modified
Mathlib/CategoryTheory/Enriched/Opposite.lean
Modified
Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
Modified
Mathlib/CategoryTheory/Equivalence.lean
Modified
Mathlib/CategoryTheory/Equivalence/Symmetry.lean
Modified
Mathlib/CategoryTheory/EssentialImage.lean
Modified
Mathlib/CategoryTheory/EssentiallySmall.lean
Modified
Mathlib/CategoryTheory/Extensive.lean
Modified
Mathlib/CategoryTheory/ExtremalEpi.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/Fiber.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean
Modified
Mathlib/CategoryTheory/Filtered/Basic.lean
Modified
Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
Modified
Mathlib/CategoryTheory/Filtered/Final.lean
Modified
Mathlib/CategoryTheory/FinCategory/AsType.lean
Modified
Mathlib/CategoryTheory/FinCategory/Basic.lean
Modified
Mathlib/CategoryTheory/FintypeCat.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/Derived/RightDerived.lean
Modified
Mathlib/CategoryTheory/Functor/EpiMono.lean
Modified
Mathlib/CategoryTheory/Functor/Flat.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean
Modified
Mathlib/CategoryTheory/Functor/TwoSquare.lean
Modified
Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean
Modified
Mathlib/CategoryTheory/Galois/Basic.lean
Modified
Mathlib/CategoryTheory/Galois/Decomposition.lean
Modified
Mathlib/CategoryTheory/Galois/EssSurj.lean
Modified
Mathlib/CategoryTheory/Galois/Full.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/HomologicalComplex.lean
Modified
Mathlib/CategoryTheory/Generator/Presheaf.lean
Modified
Mathlib/CategoryTheory/Generator/Sheaf.lean
Modified
Mathlib/CategoryTheory/Generator/StrongGenerator.lean
Modified
Mathlib/CategoryTheory/GlueData.lean
Modified
Mathlib/CategoryTheory/GradedObject.lean
Modified
Mathlib/CategoryTheory/GradedObject/Associator.lean
Modified
Mathlib/CategoryTheory/GradedObject/Bifunctor.lean
Modified
Mathlib/CategoryTheory/GradedObject/Trifunctor.lean
Modified
Mathlib/CategoryTheory/GradedObject/Unitor.lean
Modified
Mathlib/CategoryTheory/Grothendieck.lean
Modified
Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
Modified
Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean
Modified
Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean
Modified
Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
Modified
Mathlib/CategoryTheory/GuitartExact/Basic.lean
Modified
Mathlib/CategoryTheory/GuitartExact/KanExtension.lean
Modified
Mathlib/CategoryTheory/GuitartExact/Opposite.lean
Modified
Mathlib/CategoryTheory/GuitartExact/Over.lean
Modified
Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
Modified
Mathlib/CategoryTheory/Idempotents/Basic.lean
Modified
Mathlib/CategoryTheory/Idempotents/Biproducts.lean
Modified
Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean
Modified
Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean
Modified
Mathlib/CategoryTheory/Idempotents/Karoubi.lean
Modified
Mathlib/CategoryTheory/Iso.lean
Modified
Mathlib/CategoryTheory/IsomorphismClasses.lean
Modified
Mathlib/CategoryTheory/Join/Basic.lean
Modified
Mathlib/CategoryTheory/Join/Pseudofunctor.lean
Modified
Mathlib/CategoryTheory/Join/Sum.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/Basic.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/Limits.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/Over.lean
Modified
Mathlib/CategoryTheory/LiftingProperties/ParametrizedAdjunction.lean
Modified
Mathlib/CategoryTheory/Limits/Bicones.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
Modified
Mathlib/CategoryTheory/Limits/Connected.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/Filtered.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/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/WidePullbackOfTerminal.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
Modified
Mathlib/CategoryTheory/Limits/Creates.lean
Modified
Mathlib/CategoryTheory/Limits/Elements.lean
Modified
Mathlib/CategoryTheory/Limits/Filtered.lean
Modified
Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
Modified
Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/Final/Type.lean
Modified
Mathlib/CategoryTheory/Limits/FormalCoproducts/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/FormalCoproducts/Cech.lean
Modified
Mathlib/CategoryTheory/Limits/Fubini.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Kernels.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.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/FilteredColimits.lean
Modified
Mathlib/CategoryTheory/Limits/Indization/IndObject.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/Opposites.lean
Modified
Mathlib/CategoryTheory/Limits/Over.lean
Modified
Mathlib/CategoryTheory/Limits/Presentation.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Filtered.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/Biproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.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
added
theorem
CategoryTheory.Limits.coprod.leftUnitor_naturality
added
theorem
CategoryTheory.Limits.coprod.rightUnitor_naturality
Modified
Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/CombinedProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.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
deleted
def
CategoryTheory.IsKernelPair.toCoequalizer
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/NormalMono/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Kernels.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Preorder/TransfiniteCompositionOfShape.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.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/Connected.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/EquifiberedLimits.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/BicartesianSq.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Defs.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.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/StrictInitial.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Terminal.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/Shapes/ZeroObjects.lean
Modified
Mathlib/CategoryTheory/Limits/Sifted.lean
Modified
Mathlib/CategoryTheory/Limits/SmallComplete.lean
Modified
Mathlib/CategoryTheory/Limits/Types/ColimitType.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Colimits.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Coproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Filtered.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Images.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Multicoequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Pushouts.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Yoneda.lean
Modified
Mathlib/CategoryTheory/Limits/VanKampen.lean
Modified
Mathlib/CategoryTheory/Limits/Yoneda.lean
Modified
Mathlib/CategoryTheory/Linear/Basic.lean
Modified
Mathlib/CategoryTheory/Linear/LinearFunctor.lean
Modified
Mathlib/CategoryTheory/Localization/Adjunction.lean
Modified
Mathlib/CategoryTheory/Localization/Bifunctor.lean
Modified
Mathlib/CategoryTheory/Localization/Bousfield.lean
Modified
Mathlib/CategoryTheory/Localization/BousfieldTransfiniteComposition.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions/ComposableArrows.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/PointwiseRightDerived.lean
Modified
Mathlib/CategoryTheory/Localization/HomEquiv.lean
Modified
Mathlib/CategoryTheory/Localization/Linear.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/SmallHom.lean
Modified
Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
Modified
Mathlib/CategoryTheory/Localization/StructuredArrow.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/End.lean
Modified
Mathlib/CategoryTheory/Monoidal/Action/Opposites.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/Reflection.lean
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Transport.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/CommMon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Over.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/Groupoid.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/FunctorToTypes.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Ideal.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Zero.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommMon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Comon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution/Braided.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution/Closed.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution/DayFunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Discrete.lean
Modified
Mathlib/CategoryTheory/Monoidal/End.lean
Modified
Mathlib/CategoryTheory/Monoidal/Free/Basic.lean
deleted
def
CategoryTheory.FreeMonoidalCategory.setoidHom
Modified
Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
Modified
Mathlib/CategoryTheory/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Functor/Types.lean
Modified
Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Grp_.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/Internal/Types/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.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/Preadditive.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/Basic.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/Descent.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Factorization.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Ind.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Limits.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Quotient.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Representable.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Retract.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/ColimitsOfShape.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/PreservesLimits.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/Local.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/Shift.lean
Modified
Mathlib/CategoryTheory/Opposites.lean
Modified
Mathlib/CategoryTheory/PUnit.lean
Modified
Mathlib/CategoryTheory/PathCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Pi/Basic.lean
Modified
Mathlib/CategoryTheory/Pi/Monoidal.lean
Modified
Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
Modified
Mathlib/CategoryTheory/Preadditive/Basic.lean
Modified
Mathlib/CategoryTheory/Preadditive/Biproducts.lean
Modified
Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
Modified
Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
Modified
Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean
Modified
Mathlib/CategoryTheory/Preadditive/Injective/Preserves.lean
Modified
Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean
Modified
Mathlib/CategoryTheory/Preadditive/LiftToFinset.lean
Modified
Mathlib/CategoryTheory/Preadditive/Mat.lean
Modified
Mathlib/CategoryTheory/Preadditive/OfBiproducts.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/ColimitPresentation.lean
Modified
Mathlib/CategoryTheory/Presentable/Limits.lean
Modified
Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean
Modified
Mathlib/CategoryTheory/Presentable/Retracts.lean
Modified
Mathlib/CategoryTheory/Presentable/StrongGenerator.lean
Modified
Mathlib/CategoryTheory/Products/Basic.lean
Modified
Mathlib/CategoryTheory/Quotient.lean
Modified
Mathlib/CategoryTheory/Quotient/Linear.lean
Modified
Mathlib/CategoryTheory/RegularCategory/Basic.lean
Modified
Mathlib/CategoryTheory/RepresentedBy.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/Quotient.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/Twist.lean
Modified
Mathlib/CategoryTheory/ShrinkYoneda.lean
Modified
Mathlib/CategoryTheory/Sigma/Basic.lean
Modified
Mathlib/CategoryTheory/SingleObj.lean
Modified
Mathlib/CategoryTheory/Sites/Abelian.lean
Modified
Mathlib/CategoryTheory/Sites/Adjunction.lean
Modified
Mathlib/CategoryTheory/Sites/CartesianMonoidal.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/ReflectsPrecoherent.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/ReflectsPreregular.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.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/CoversTop.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean
Modified
Mathlib/CategoryTheory/Sites/Descent/DescentData.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/Hypercover/Homotopy.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/One.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/Subcanonical.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/ZeroFamily.lean
Modified
Mathlib/CategoryTheory/Sites/IsSheafFor.lean
Modified
Mathlib/CategoryTheory/Sites/LeftExact.lean
Modified
Mathlib/CategoryTheory/Sites/Limits.lean
Modified
Mathlib/CategoryTheory/Sites/LocallyBijective.lean
Modified
Mathlib/CategoryTheory/Sites/LocallyInjective.lean
Modified
Mathlib/CategoryTheory/Sites/LocallySurjective.lean
Modified
Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean
Modified
Mathlib/CategoryTheory/Sites/Monoidal.lean
Modified
Mathlib/CategoryTheory/Sites/Over.lean
Modified
Mathlib/CategoryTheory/Sites/Plus.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Point/Over.lean
Modified
Mathlib/CategoryTheory/Sites/Precoverage.lean
Modified
Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean
Modified
Mathlib/CategoryTheory/Sites/Preserves.lean
Modified
Mathlib/CategoryTheory/Sites/PreservesLocallyBijective.lean
Modified
Mathlib/CategoryTheory/Sites/PreservesSheafification.lean
Modified
Mathlib/CategoryTheory/Sites/Pretopology.lean
Modified
Mathlib/CategoryTheory/Sites/RegularEpi.lean
Modified
Mathlib/CategoryTheory/Sites/Sheaf.lean
Modified
Mathlib/CategoryTheory/Sites/SheafCohomology/MayerVietoris.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/Spaces.lean
Modified
Mathlib/CategoryTheory/Sites/Types.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/ExtendToSucc.lean
Modified
Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
Modified
Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
Modified
Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
Modified
Mathlib/CategoryTheory/Square.lean
Modified
Mathlib/CategoryTheory/Subfunctor/Basic.lean
Modified
Mathlib/CategoryTheory/Subfunctor/Equalizer.lean
Modified
Mathlib/CategoryTheory/Subfunctor/Finite.lean
Modified
Mathlib/CategoryTheory/Subfunctor/Image.lean
Modified
Mathlib/CategoryTheory/Subfunctor/OfSection.lean
Modified
Mathlib/CategoryTheory/Subobject/ArtinianObject.lean
Modified
Mathlib/CategoryTheory/Subobject/Basic.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/Subterminal.lean
Modified
Mathlib/CategoryTheory/Sums/Associator.lean
Modified
Mathlib/CategoryTheory/Sums/Basic.lean
Modified
Mathlib/CategoryTheory/Sums/Products.lean
Modified
Mathlib/CategoryTheory/Topos/Classifier.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/Opposite/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/OpOp.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean
Modified
Mathlib/CategoryTheory/Triangulated/Opposite/Triangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Orthogonal.lean
Modified
Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Rotate.lean
Modified
Mathlib/CategoryTheory/Triangulated/SpectralObject.lean
Modified
Mathlib/CategoryTheory/Triangulated/Subcategory.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean
Modified
Mathlib/CategoryTheory/Triangulated/TriangleShift.lean
Modified
Mathlib/CategoryTheory/Triangulated/Triangulated.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/AP/Three/Behrend.lean
Modified
Mathlib/Combinatorics/Additive/CauchyDavenport.lean
Modified
Mathlib/Combinatorics/Additive/Convolution.lean
Modified
Mathlib/Combinatorics/Additive/Corner/Roth.lean
Modified
Mathlib/Combinatorics/Additive/Dissociation.lean
Modified
Mathlib/Combinatorics/Additive/DoublingConst.lean
Modified
Mathlib/Combinatorics/Additive/ETransform.lean
Modified
Mathlib/Combinatorics/Additive/Energy.lean
Modified
Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
Modified
Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
Modified
Mathlib/Combinatorics/Additive/Randomisation.lean
Modified
Mathlib/Combinatorics/Additive/RuzsaCovering.lean
Modified
Mathlib/Combinatorics/Additive/SmallTripling.lean
Modified
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
Modified
Mathlib/Combinatorics/Colex.lean
Modified
Mathlib/Combinatorics/Configuration.lean
Modified
Mathlib/Combinatorics/Derangements/Finite.lean
Modified
Mathlib/Combinatorics/Enumerative/Bell.lean
Modified
Mathlib/Combinatorics/Enumerative/Catalan.lean
Modified
Mathlib/Combinatorics/Enumerative/Composition.lean
Modified
Mathlib/Combinatorics/Enumerative/DyckWord.lean
Modified
Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
Modified
Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
Modified
Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean
Modified
Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean
Modified
Mathlib/Combinatorics/Enumerative/Schroder.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/Circuit.lean
Modified
Mathlib/Combinatorics/Matroid/Closure.lean
Modified
Mathlib/Combinatorics/Matroid/Dual.lean
Modified
Mathlib/Combinatorics/Matroid/Loop.lean
Modified
Mathlib/Combinatorics/Matroid/Map.lean
Modified
Mathlib/Combinatorics/Matroid/Minor/Contract.lean
Modified
Mathlib/Combinatorics/Matroid/Minor/Delete.lean
Modified
Mathlib/Combinatorics/Matroid/Rank/ENat.lean
Modified
Mathlib/Combinatorics/Matroid/Sum.lean
Modified
Mathlib/Combinatorics/Nullstellensatz.lean
Modified
Mathlib/Combinatorics/Quiver/Covering.lean
Modified
Mathlib/Combinatorics/Quiver/Path.lean
Modified
Mathlib/Combinatorics/Quiver/SingleObj.lean
Modified
Mathlib/Combinatorics/Quiver/Symmetric.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/SetFamily/LYM.lean
Modified
Mathlib/Combinatorics/SetFamily/Shatter.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/Circulant.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Coloring.lean
Modified
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Copy.lean
Modified
Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean
Modified
Mathlib/Combinatorics/SimpleGraph/EdgeLabeling.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Finite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Girth.lean
Modified
Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Maps.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Matching.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Operations.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Partition.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Prod.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean
Modified
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Tutte.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walks/Subwalks.lean
Modified
Mathlib/Combinatorics/Tiling/Tile.lean
Modified
Mathlib/Computability/Ackermann.lean
Modified
Mathlib/Computability/AkraBazzi/AkraBazzi.lean
Modified
Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
Modified
Mathlib/Computability/AkraBazzi/SumTransform.lean
Modified
Mathlib/Computability/ContextFreeGrammar.lean
Modified
Mathlib/Computability/DFA.lean
Modified
Mathlib/Computability/Halting.lean
Modified
Mathlib/Computability/MyhillNerode.lean
Modified
Mathlib/Computability/NFA.lean
Modified
Mathlib/Computability/PostTuringMachine.lean
Modified
Mathlib/Computability/Primrec/Basic.lean
Modified
Mathlib/Computability/Primrec/List.lean
Modified
Mathlib/Computability/Reduce.lean
Modified
Mathlib/Computability/TMConfig.lean
Modified
Mathlib/Computability/TMToPartrec.lean
Modified
Mathlib/Computability/TuringMachine.lean
Modified
Mathlib/Condensed/Discrete/Characterization.lean
Modified
Mathlib/Condensed/Discrete/Colimit.lean
Modified
Mathlib/Condensed/Discrete/LocallyConstant.lean
Modified
Mathlib/Condensed/Discrete/Module.lean
Modified
Mathlib/Condensed/Epi.lean
Modified
Mathlib/Condensed/Light/Epi.lean
Modified
Mathlib/Condensed/Light/InternallyProjective.lean
Modified
Mathlib/Condensed/Light/Monoidal.lean
Modified
Mathlib/Condensed/Light/Small.lean
Modified
Mathlib/Condensed/Light/TopCatAdjunction.lean
Modified
Mathlib/Condensed/TopCatAdjunction.lean
Modified
Mathlib/Condensed/TopComparison.lean
Modified
Mathlib/Control/Bitraversable/Instances.lean
Modified
Mathlib/Control/Fold.lean
Modified
Mathlib/Control/Functor/Multivariate.lean
Modified
Mathlib/Data/BitVec.lean
Modified
Mathlib/Data/Bool/Count.lean
Modified
Mathlib/Data/Complex/Basic.lean
Modified
Mathlib/Data/DFinsupp/Defs.lean
Modified
Mathlib/Data/DFinsupp/Encodable.lean
Modified
Mathlib/Data/DFinsupp/Lex.lean
Modified
Mathlib/Data/DFinsupp/Order.lean
Modified
Mathlib/Data/DFinsupp/Sigma.lean
Modified
Mathlib/Data/ENNReal/Action.lean
Modified
Mathlib/Data/ENNReal/Basic.lean
deleted
def
ENNReal.ofNNRealHom
Modified
Mathlib/Data/ENNReal/BigOperators.lean
Modified
Mathlib/Data/ENNReal/Operations.lean
Modified
Mathlib/Data/ENNReal/Real.lean
deleted
def
ENNReal.toNNRealHom
deleted
def
ENNReal.toRealHom
Modified
Mathlib/Data/ENat/Basic.lean
Modified
Mathlib/Data/ENat/Pow.lean
Modified
Mathlib/Data/EReal/Basic.lean
Modified
Mathlib/Data/EReal/Inv.lean
Modified
Mathlib/Data/EReal/Operations.lean
Modified
Mathlib/Data/Erased.lean
Modified
Mathlib/Data/Fin/Tuple/Basic.lean
Modified
Mathlib/Data/Fin/Tuple/Sort.lean
Modified
Mathlib/Data/Fin/Tuple/Take.lean
Modified
Mathlib/Data/FinEnum.lean
Modified
Mathlib/Data/Finset/Attach.lean
Modified
Mathlib/Data/Finset/Basic.lean
Modified
Mathlib/Data/Finset/Card.lean
Modified
Mathlib/Data/Finset/Disjoint.lean
Modified
Mathlib/Data/Finset/Filter.lean
Modified
Mathlib/Data/Finset/Fin.lean
Modified
Mathlib/Data/Finset/Image.lean
Modified
Mathlib/Data/Finset/Insert.lean
Modified
Mathlib/Data/Finset/Lattice/Fold.lean
Modified
Mathlib/Data/Finset/Max.lean
Modified
Mathlib/Data/Finset/NatAntidiagonal.lean
Modified
Mathlib/Data/Finset/NoncommProd.lean
Modified
Mathlib/Data/Finset/Pi.lean
Modified
Mathlib/Data/Finset/Powerset.lean
Modified
Mathlib/Data/Finset/Preimage.lean
Modified
Mathlib/Data/Finset/Sort.lean
Modified
Mathlib/Data/Finset/Sum.lean
Modified
Mathlib/Data/Finset/Sups.lean
Modified
Mathlib/Data/Finset/Sym.lean
Modified
Mathlib/Data/Finset/SymmDiff.lean
Modified
Mathlib/Data/Finset/Union.lean
Modified
Mathlib/Data/Finset/Update.lean
Modified
Mathlib/Data/Finsupp/AList.lean
Modified
Mathlib/Data/Finsupp/Indicator.lean
Modified
Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
Modified
Mathlib/Data/Finsupp/Order.lean
Modified
Mathlib/Data/Finsupp/PointwiseSMul.lean
Modified
Mathlib/Data/Finsupp/SMul.lean
Modified
Mathlib/Data/Finsupp/Single.lean
Modified
Mathlib/Data/Finsupp/Weight.lean
Modified
Mathlib/Data/Fintype/BigOperators.lean
Modified
Mathlib/Data/Fintype/Defs.lean
Modified
Mathlib/Data/Fintype/EquivFin.lean
Modified
Mathlib/Data/Fintype/Sets.lean
Modified
Mathlib/Data/Fintype/Units.lean
Modified
Mathlib/Data/Holor.lean
Modified
Mathlib/Data/Int/CardIntervalMod.lean
Modified
Mathlib/Data/Int/Fib/Basic.lean
Modified
Mathlib/Data/Int/Fib/Lemmas.lean
Modified
Mathlib/Data/Int/GCD.lean
Modified
Mathlib/Data/Int/Init.lean
deleted
theorem
Int.ext_ediv_emod
deleted
theorem
Int.ext_ediv_emod_iff
Modified
Mathlib/Data/Int/Order/Basic.lean
Modified
Mathlib/Data/Int/Star.lean
Modified
Mathlib/Data/Int/SuccPred.lean
Modified
Mathlib/Data/List/MinMax.lean
Modified
Mathlib/Data/List/NodupEquivFin.lean
Modified
Mathlib/Data/List/OfFn.lean
deleted
theorem
List.map_ofFn
deleted
theorem
List.ofFn_getElem
Modified
Mathlib/Data/List/Pi.lean
Modified
Mathlib/Data/List/Shortlex.lean
Modified
Mathlib/Data/List/SplitLengths.lean
Modified
Mathlib/Data/Matrix/Basic.lean
Modified
Mathlib/Data/Matrix/Basis.lean
Modified
Mathlib/Data/Matrix/DualNumber.lean
Modified
Mathlib/Data/Matrix/Invertible.lean
Modified
Mathlib/Data/Matrix/PEquiv.lean
Modified
Mathlib/Data/Multiset/Fintype.lean
Modified
Mathlib/Data/Multiset/Interval.lean
Modified
Mathlib/Data/NNRat/Defs.lean
Modified
Mathlib/Data/NNReal/Basic.lean
Modified
Mathlib/Data/NNReal/Defs.lean
Modified
Mathlib/Data/Nat/Basic.lean
Modified
Mathlib/Data/Nat/Bitwise.lean
Modified
Mathlib/Data/Nat/Cast/Order/Ring.lean
Modified
Mathlib/Data/Nat/Choose/Central.lean
Modified
Mathlib/Data/Nat/Choose/Factorization.lean
Modified
Mathlib/Data/Nat/Choose/Multinomial.lean
Modified
Mathlib/Data/Nat/Choose/Sum.lean
Modified
Mathlib/Data/Nat/Choose/Vandermonde.lean
Modified
Mathlib/Data/Nat/Count.lean
Modified
Mathlib/Data/Nat/Digits/Lemmas.lean
Modified
Mathlib/Data/Nat/Factorization/Basic.lean
Modified
Mathlib/Data/Nat/Factorization/Defs.lean
Modified
Mathlib/Data/Nat/Factorization/LCM.lean
Modified
Mathlib/Data/Nat/Factorization/PrimePow.lean
Modified
Mathlib/Data/Nat/Factorization/Root.lean
Modified
Mathlib/Data/Nat/Fib/Basic.lean
Modified
Mathlib/Data/Nat/Fib/Zeckendorf.lean
Modified
Mathlib/Data/Nat/GCD/Basic.lean
Modified
Mathlib/Data/Nat/Init.lean
deleted
theorem
Nat.ext_div_mod
deleted
theorem
Nat.ext_div_mod_iff
Modified
Mathlib/Data/Nat/ModEq.lean
Modified
Mathlib/Data/Nat/Multiplicity.lean
Modified
Mathlib/Data/Nat/Prime/Defs.lean
Modified
Mathlib/Data/Nat/Squarefree.lean
Modified
Mathlib/Data/Nat/SuccPred.lean
Modified
Mathlib/Data/Nat/Totient.lean
Modified
Mathlib/Data/Num/Lemmas.lean
Modified
Mathlib/Data/Num/Prime.lean
Modified
Mathlib/Data/Num/ZNum.lean
Modified
Mathlib/Data/Ordmap/Invariants.lean
Modified
Mathlib/Data/Ordmap/Ordset.lean
Modified
Mathlib/Data/PFunctor/Multivariate/M.lean
Modified
Mathlib/Data/PFunctor/Multivariate/W.lean
Modified
Mathlib/Data/PFunctor/Univariate/M.lean
Modified
Mathlib/Data/PNat/Basic.lean
Modified
Mathlib/Data/PNat/Factors.lean
Modified
Mathlib/Data/PNat/Interval.lean
Modified
Mathlib/Data/Prod/Lex.lean
Modified
Mathlib/Data/Prod/TProd.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Sigma.lean
Modified
Mathlib/Data/QPF/Univariate/Basic.lean
Modified
Mathlib/Data/Rat/Cast/Order.lean
Modified
Mathlib/Data/Rat/Defs.lean
deleted
theorem
Rat.eq_iff_mul_eq_mul
Modified
Mathlib/Data/Rat/Floor.lean
Modified
Mathlib/Data/Rat/NatSqrt/Defs.lean
Modified
Mathlib/Data/Rat/NatSqrt/Real.lean
Modified
Mathlib/Data/Rat/Star.lean
Modified
Mathlib/Data/Real/Archimedean.lean
Modified
Mathlib/Data/Real/Embedding.lean
Modified
Mathlib/Data/Real/StarOrdered.lean
Modified
Mathlib/Data/Semiquot.lean
Modified
Mathlib/Data/Seq/Basic.lean
Modified
Mathlib/Data/Seq/Defs.lean
Modified
Mathlib/Data/Seq/Parallel.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Set/Card/Arithmetic.lean
Modified
Mathlib/Data/Set/Finite/Basic.lean
Modified
Mathlib/Data/Set/Function.lean
Modified
Mathlib/Data/Set/Functor.lean
Modified
Mathlib/Data/Set/Image.lean
Modified
Mathlib/Data/Set/MemPartition.lean
Modified
Mathlib/Data/Set/Pairwise/Basic.lean
Modified
Mathlib/Data/Set/Pairwise/Lattice.lean
Modified
Mathlib/Data/Set/PowersetCard.lean
Modified
Mathlib/Data/Set/Prod.lean
Modified
Mathlib/Data/Set/Semiring.lean
deleted
def
SetSemiring.singletonMonoidHom
Modified
Mathlib/Data/Set/Sups.lean
Modified
Mathlib/Data/Setoid/Basic.lean
Modified
Mathlib/Data/Setoid/Partition.lean
Modified
Mathlib/Data/Sign/Basic.lean
Modified
Mathlib/Data/String/Basic.lean
Modified
Mathlib/Data/Sum/Order.lean
Modified
Mathlib/Data/Sym/Basic.lean
Modified
Mathlib/Data/Sym/Sym2.lean
Modified
Mathlib/Data/Sym/Sym2/Finsupp.lean
Modified
Mathlib/Data/TypeVec.lean
Modified
Mathlib/Data/Vector/Basic.lean
Modified
Mathlib/Data/Vector/Mem.lean
Modified
Mathlib/Data/WSeq/Basic.lean
Modified
Mathlib/Data/ZMod/Basic.lean
Modified
Mathlib/Data/ZMod/Coprime.lean
Modified
Mathlib/Data/ZMod/Defs.lean
Modified
Mathlib/Data/ZMod/IntUnitsPower.lean
Modified
Mathlib/Data/ZMod/QuotientGroup.lean
Modified
Mathlib/Data/ZMod/Units.lean
Modified
Mathlib/Data/ZMod/ValMinAbs.lean
Modified
Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
Modified
Mathlib/Dynamics/Ergodic/AddCircle.lean
Modified
Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
Modified
Mathlib/Dynamics/PeriodicPts/Lemmas.lean
Modified
Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
Modified
Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
Modified
Mathlib/FieldTheory/AbelRuffini.lean
Modified
Mathlib/FieldTheory/AbsoluteGaloisGroup.lean
Modified
Mathlib/FieldTheory/AlgebraicClosure.lean
Modified
Mathlib/FieldTheory/AxGrothendieck.lean
Modified
Mathlib/FieldTheory/CardinalEmb.lean
Modified
Mathlib/FieldTheory/ChevalleyWarning.lean
Modified
Mathlib/FieldTheory/Differential/Basic.lean
Modified
Mathlib/FieldTheory/Differential/Liouville.lean
Modified
Mathlib/FieldTheory/Extension.lean
Modified
Mathlib/FieldTheory/Finite/Basic.lean
Modified
Mathlib/FieldTheory/Finite/GaloisField.lean
Modified
Mathlib/FieldTheory/Finite/Polynomial.lean
Modified
Mathlib/FieldTheory/Fixed.lean
Modified
Mathlib/FieldTheory/Galois/Abelian.lean
Modified
Mathlib/FieldTheory/Galois/Basic.lean
Modified
Mathlib/FieldTheory/Galois/GaloisClosure.lean
Modified
Mathlib/FieldTheory/Galois/Infinite.lean
Modified
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
Modified
Mathlib/FieldTheory/Galois/NormalBasis.lean
Modified
Mathlib/FieldTheory/Galois/Profinite.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
Modified
Mathlib/FieldTheory/IntermediateField/Algebraic.lean
Modified
Mathlib/FieldTheory/IntermediateField/Basic.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/Classification.lean
Modified
Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
Modified
Mathlib/FieldTheory/IsPerfectClosure.lean
Modified
Mathlib/FieldTheory/Isaacs.lean
Modified
Mathlib/FieldTheory/JacobsonNoether.lean
Modified
Mathlib/FieldTheory/KrullTopology.lean
Modified
Mathlib/FieldTheory/KummerExtension.lean
Modified
Mathlib/FieldTheory/LinearDisjoint.lean
Modified
Mathlib/FieldTheory/Minpoly/Basic.lean
Modified
Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
Modified
Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
Modified
Mathlib/FieldTheory/MvRatFunc/Rank.lean
Modified
Mathlib/FieldTheory/Normal/Basic.lean
Modified
Mathlib/FieldTheory/Normal/Closure.lean
Modified
Mathlib/FieldTheory/Normal/Defs.lean
Modified
Mathlib/FieldTheory/NormalizedTrace.lean
Modified
Mathlib/FieldTheory/PolynomialGaloisGroup.lean
Modified
Mathlib/FieldTheory/PrimeField.lean
Modified
Mathlib/FieldTheory/PrimitiveElement.lean
Modified
Mathlib/FieldTheory/PurelyInseparable/Basic.lean
Modified
Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
Modified
Mathlib/FieldTheory/PurelyInseparable/Tower.lean
Modified
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
Modified
Mathlib/FieldTheory/RatFunc/Basic.lean
Modified
Mathlib/FieldTheory/RatFunc/Degree.lean
Modified
Mathlib/FieldTheory/Relrank.lean
Modified
Mathlib/FieldTheory/Separable.lean
Modified
Mathlib/FieldTheory/SeparableClosure.lean
Modified
Mathlib/FieldTheory/SeparableDegree.lean
Modified
Mathlib/FieldTheory/SeparablyGenerated.lean
Modified
Mathlib/FieldTheory/SplittingField/Construction.lean
Modified
Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
Modified
Mathlib/Geometry/Convex/Cone/Basic.lean
Modified
Mathlib/Geometry/Convex/Cone/Dual.lean
Modified
Mathlib/Geometry/Convex/Cone/Pointed.lean
Modified
Mathlib/Geometry/Diffeology/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Altitude.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Sphere.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean
Modified
Mathlib/Geometry/Euclidean/Circumcenter.lean
Modified
Mathlib/Geometry/Euclidean/Incenter.lean
Modified
Mathlib/Geometry/Euclidean/MongePoint.lean
Modified
Mathlib/Geometry/Euclidean/NinePointCircle.lean
Modified
Mathlib/Geometry/Euclidean/PerpBisector.lean
Modified
Mathlib/Geometry/Euclidean/Projection.lean
Modified
Mathlib/Geometry/Euclidean/SignedDist.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean
deleted
def
EuclideanGeometry.Sphere.orthRadius
Modified
Mathlib/Geometry/Euclidean/Sphere/Power.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/Tangent.lean
Modified
Mathlib/Geometry/Euclidean/Triangle.lean
Modified
Mathlib/Geometry/Group/Growth/LinearLowerBound.lean
Modified
Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
Modified
Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
Modified
Mathlib/Geometry/Manifold/Algebra/Monoid.lean
Modified
Mathlib/Geometry/Manifold/Algebra/Structures.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/ContMDiffMFDeriv.lean
Modified
Mathlib/Geometry/Manifold/DerivationBundle.lean
Modified
Mathlib/Geometry/Manifold/Diffeomorph.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/Instances/UnitsOfNormedAlgebra.lean
Modified
Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
Modified
Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.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/LocalDiffeomorph.lean
Modified
Mathlib/Geometry/Manifold/LocalInvariantProperties.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/MFDeriv/UniqueDifferential.lean
Modified
Mathlib/Geometry/Manifold/PartitionOfUnity.lean
Modified
Mathlib/Geometry/Manifold/Riemannian/Basic.lean
Modified
Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
Modified
Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/Hom.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.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/Archimedean.lean
Modified
Mathlib/GroupTheory/ArchimedeanDensely.lean
Modified
Mathlib/GroupTheory/Commensurable.lean
Modified
Mathlib/GroupTheory/Commutator/Basic.lean
Modified
Mathlib/GroupTheory/Commutator/Finite.lean
Modified
Mathlib/GroupTheory/CommutingProbability.lean
Modified
Mathlib/GroupTheory/Complement.lean
Modified
Mathlib/GroupTheory/Congruence/Defs.lean
Modified
Mathlib/GroupTheory/Congruence/Hom.lean
Modified
Mathlib/GroupTheory/Coprod/Basic.lean
Modified
Mathlib/GroupTheory/CoprodI.lean
Modified
Mathlib/GroupTheory/Coset/Basic.lean
Modified
Mathlib/GroupTheory/Coset/Defs.lean
Modified
Mathlib/GroupTheory/CosetCover.lean
Modified
Mathlib/GroupTheory/Coxeter/Basic.lean
Modified
Mathlib/GroupTheory/Coxeter/Inversion.lean
Modified
Mathlib/GroupTheory/Divisible.lean
Modified
Mathlib/GroupTheory/DivisibleHull.lean
Modified
Mathlib/GroupTheory/DoubleCoset.lean
Modified
Mathlib/GroupTheory/Exponent.lean
Modified
Mathlib/GroupTheory/Frattini.lean
Modified
Mathlib/GroupTheory/FreeAbelianGroup.lean
Modified
Mathlib/GroupTheory/FreeGroup/Basic.lean
Modified
Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
Modified
Mathlib/GroupTheory/FreeGroup/Orbit.lean
Modified
Mathlib/GroupTheory/GroupAction/Basic.lean
Modified
Mathlib/GroupTheory/GroupAction/Blocks.lean
Modified
Mathlib/GroupTheory/GroupAction/Defs.lean
Modified
Mathlib/GroupTheory/GroupAction/FixedPoints.lean
Modified
Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
Modified
Mathlib/GroupTheory/GroupAction/Iwasawa.lean
Modified
Mathlib/GroupTheory/GroupAction/Jordan.lean
Modified
Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean
Modified
Mathlib/GroupTheory/GroupAction/Primitive.lean
Modified
Mathlib/GroupTheory/GroupAction/Quotient.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean
Modified
Mathlib/GroupTheory/HNNExtension.lean
Modified
Mathlib/GroupTheory/Index.lean
Modified
Mathlib/GroupTheory/IsSubnormal.lean
Modified
Mathlib/GroupTheory/MonoidLocalization/Basic.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/Closure.lean
Modified
Mathlib/GroupTheory/Perm/ClosureSwap.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/DomMulAct.lean
Modified
Mathlib/GroupTheory/Perm/Fin.lean
Modified
Mathlib/GroupTheory/Perm/Finite.lean
Modified
Mathlib/GroupTheory/Perm/List.lean
Modified
Mathlib/GroupTheory/Perm/MaximalSubgroups.lean
Modified
Mathlib/GroupTheory/Perm/Support.lean
Modified
Mathlib/GroupTheory/PresentedGroup.lean
Modified
Mathlib/GroupTheory/PushoutI.lean
Modified
Mathlib/GroupTheory/QuotientGroup/Basic.lean
Modified
Mathlib/GroupTheory/QuotientGroup/Finite.lean
Modified
Mathlib/GroupTheory/Schreier.lean
Modified
Mathlib/GroupTheory/SchurZassenhaus.lean
Modified
Mathlib/GroupTheory/SemidirectProduct.lean
Modified
Mathlib/GroupTheory/Solvable.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating/KleinFour.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
Modified
Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
Modified
Mathlib/GroupTheory/Subgroup/Centralizer.lean
Modified
Mathlib/GroupTheory/Subgroup/Simple.lean
Modified
Mathlib/GroupTheory/Sylow.lean
Modified
Mathlib/GroupTheory/Torsion.lean
Modified
Mathlib/GroupTheory/Transfer.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Basis.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Centroid.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Ceva.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Combination.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Independent.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Restrict.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
Modified
Mathlib/LinearAlgebra/Alternating/Basic.lean
Modified
Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
Modified
Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean
Modified
Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
Modified
Mathlib/LinearAlgebra/Basis/Defs.lean
Modified
Mathlib/LinearAlgebra/Basis/Exact.lean
Modified
Mathlib/LinearAlgebra/Basis/Fin.lean
Modified
Mathlib/LinearAlgebra/Basis/VectorSpace.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
Modified
Mathlib/LinearAlgebra/Center.lean
Modified
Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
Modified
Mathlib/LinearAlgebra/Coevaluation.lean
Modified
Mathlib/LinearAlgebra/Complex/Determinant.lean
Modified
Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean
Modified
Mathlib/LinearAlgebra/Complex/Module.lean
Modified
Mathlib/LinearAlgebra/CrossProduct.lean
Modified
Mathlib/LinearAlgebra/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/Determinant.lean
Modified
Mathlib/LinearAlgebra/Dimension/Constructions.lean
Modified
Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
Modified
Mathlib/LinearAlgebra/Dimension/Finite.lean
Modified
Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
Modified
Mathlib/LinearAlgebra/Dimension/LinearMap.lean
Modified
Mathlib/LinearAlgebra/Dimension/Localization.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/Dual/Lemmas.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Pi.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Zero.lean
Modified
Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
Modified
Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
Modified
Mathlib/LinearAlgebra/ExteriorPower/Basis.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
Modified
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean
Modified
Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
Modified
Mathlib/LinearAlgebra/Finsupp/Supported.lean
Modified
Mathlib/LinearAlgebra/FreeAlgebra.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Int.lean
Modified
Mathlib/LinearAlgebra/FreeModule/ModN.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Norm.lean
Modified
Mathlib/LinearAlgebra/FreeModule/PID.lean
Modified
Mathlib/LinearAlgebra/Goursat.lean
Modified
Mathlib/LinearAlgebra/Isomorphisms.lean
Modified
Mathlib/LinearAlgebra/JordanChevalley.lean
Modified
Mathlib/LinearAlgebra/LinearDisjoint.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/Adjugate.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean
Modified
Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean
Modified
Mathlib/LinearAlgebra/Matrix/Defs.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
Modified
Mathlib/LinearAlgebra/Matrix/Diagonal.lean
Modified
Mathlib/LinearAlgebra/Matrix/FiniteDimensional.lean
Modified
Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
Modified
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
Modified
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
Modified
Mathlib/LinearAlgebra/Matrix/Ideal.lean
Modified
Mathlib/LinearAlgebra/Matrix/Kronecker.lean
Modified
Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
Modified
Mathlib/LinearAlgebra/Matrix/Notation.lean
Modified
Mathlib/LinearAlgebra/Matrix/Rank.lean
Modified
Mathlib/LinearAlgebra/Matrix/RowCol.lean
Modified
Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
Modified
Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
Modified
Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLin.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
Modified
Mathlib/LinearAlgebra/Matrix/Trace.lean
Modified
Mathlib/LinearAlgebra/Matrix/Transvection.lean
Modified
Mathlib/LinearAlgebra/Multilinear/Basic.lean
Modified
Mathlib/LinearAlgebra/Multilinear/Basis.lean
Modified
Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/Multilinear/DirectSum.lean
Modified
Mathlib/LinearAlgebra/PID.lean
Modified
Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
Modified
Mathlib/LinearAlgebra/Pi.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct/DirectSum.lean
Modified
Mathlib/LinearAlgebra/Prod.lean
Modified
Mathlib/LinearAlgebra/Projection.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Basic.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Constructions.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Subspace.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Dual.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Real.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/Quotient/Basic.lean
Modified
Mathlib/LinearAlgebra/Quotient/Defs.lean
Modified
Mathlib/LinearAlgebra/Quotient/Pi.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/Basic.lean
Modified
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Chain.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Relations.lean
Modified
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Irreducible.lean
Modified
Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
Modified
Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
Modified
Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean
Modified
Mathlib/LinearAlgebra/Semisimple.lean
Modified
Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean
Modified
Mathlib/LinearAlgebra/Span/Basic.lean
Modified
Mathlib/LinearAlgebra/Span/Defs.lean
Modified
Mathlib/LinearAlgebra/Span/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/SpecialLinearGroup.lean
Modified
Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean
Modified
Mathlib/LinearAlgebra/SymplecticGroup.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
Modified
Mathlib/LinearAlgebra/TensorPower/Basic.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Basis.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Defs.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
Modified
Mathlib/LinearAlgebra/Trace.lean
Modified
Mathlib/LinearAlgebra/Transvection.lean
Modified
Mathlib/LinearAlgebra/Vandermonde.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Denumerable.lean
Modified
Mathlib/Logic/Embedding/Basic.lean
Modified
Mathlib/Logic/Encodable/Basic.lean
Modified
Mathlib/Logic/Equiv/Embedding.lean
Modified
Mathlib/Logic/Equiv/Multiset.lean
Modified
Mathlib/Logic/Equiv/Set.lean
Modified
Mathlib/Logic/Nonempty.lean
Modified
Mathlib/Logic/Small/Defs.lean
Modified
Mathlib/Logic/UnivLE.lean
Modified
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
Modified
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
Modified
Mathlib/MeasureTheory/Constructions/BorelSpace/WithTop.lean
Modified
Mathlib/MeasureTheory/Constructions/Cylinders.lean
Modified
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
Modified
Mathlib/MeasureTheory/Constructions/Pi.lean
Modified
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
Modified
Mathlib/MeasureTheory/Constructions/Projective.lean
Modified
Mathlib/MeasureTheory/Constructions/SimpleGraph.lean
Modified
Mathlib/MeasureTheory/Covering/Besicovitch.lean
Modified
Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
Modified
Mathlib/MeasureTheory/Covering/DensityTheorem.lean
Modified
Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
Modified
Mathlib/MeasureTheory/Covering/Vitali.lean
Modified
Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
Modified
Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
Modified
Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean
Modified
Mathlib/MeasureTheory/Function/EssSup.lean
Modified
Mathlib/MeasureTheory/Function/FactorsThrough.lean
Modified
Mathlib/MeasureTheory/Function/Intersectivity.lean
Modified
Mathlib/MeasureTheory/Function/Jacobian.lean
Modified
Mathlib/MeasureTheory/Function/JacobianOneDim.lean
Modified
Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
Modified
Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
Modified
Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/LpNorm.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
Modified
Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFunc.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
Modified
Mathlib/MeasureTheory/Function/UniformIntegrable.lean
Modified
Mathlib/MeasureTheory/Group/AEStabilizer.lean
Modified
Mathlib/MeasureTheory/Group/FoelnerFilter.lean
deleted
def
maxFoelner
Modified
Mathlib/MeasureTheory/Group/FundamentalDomain.lean
Modified
Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean
Modified
Mathlib/MeasureTheory/Integral/Average.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/L1.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/Set.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean
Modified
Mathlib/MeasureTheory/Integral/CircleAverage.lean
Modified
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
Modified
Mathlib/MeasureTheory/Integral/CircleTransform.lean
Modified
Mathlib/MeasureTheory/Integral/CompactlySupported.lean
Modified
Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean
Modified
Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
Modified
Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
Modified
Mathlib/MeasureTheory/Integral/Gamma.lean
Modified
Mathlib/MeasureTheory/Integral/IntegrableOn.lean
Modified
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalAverage.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Slope.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean
Modified
Mathlib/MeasureTheory/Integral/Layercake.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean
Modified
Mathlib/MeasureTheory/Integral/MeanInequalities.lean
Modified
Mathlib/MeasureTheory/Integral/PeakFunction.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/NNReal.lean
Modified
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean
Modified
Mathlib/MeasureTheory/Integral/SetToL1.lean
Modified
Mathlib/MeasureTheory/Integral/TorusIntegral.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
Modified
Mathlib/MeasureTheory/Measure/AEDisjoint.lean
Modified
Mathlib/MeasureTheory/Measure/AddContent.lean
Modified
Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean
Modified
Mathlib/MeasureTheory/Measure/Content.lean
Modified
Mathlib/MeasureTheory/Measure/Decomposition/Hahn.lean
Modified
Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
Modified
Mathlib/MeasureTheory/Measure/DiracProba.lean
Modified
Mathlib/MeasureTheory/Measure/Doubling.lean
Modified
Mathlib/MeasureTheory/Measure/EverywherePos.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/DistribChar.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Unique.lean
Modified
Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean
Modified
Mathlib/MeasureTheory/Measure/Hausdorff.lean
Modified
Mathlib/MeasureTheory/Measure/IntegralCharFun.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
Modified
Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
Modified
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
Modified
Mathlib/MeasureTheory/Measure/MeasuredSets.lean
Modified
Mathlib/MeasureTheory/Measure/MutuallySingular.lean
Modified
Mathlib/MeasureTheory/Measure/NullMeasurable.lean
Modified
Mathlib/MeasureTheory/Measure/Portmanteau.lean
Modified
Mathlib/MeasureTheory/Measure/PreVariation.lean
Modified
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Prod.lean
Modified
Mathlib/MeasureTheory/Measure/Regular.lean
Modified
Mathlib/MeasureTheory/Measure/Restrict.lean
Modified
Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Stieltjes.lean
Modified
Mathlib/MeasureTheory/Measure/Sub.lean
Modified
Mathlib/MeasureTheory/Measure/Tight.lean
Modified
Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean
Modified
Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean
Modified
Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/AE.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/Induced.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/Operations.lean
Modified
Mathlib/MeasureTheory/SetSemiring.lean
Modified
Mathlib/MeasureTheory/SpecificCodomains/ContinuousMapZero.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/AddContent.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/Decomposition/Lebesgue.lean
Modified
Mathlib/ModelTheory/Algebra/Ring/Basic.lean
Modified
Mathlib/ModelTheory/Algebra/Ring/Definability.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Basic.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Basic.lean
Modified
Mathlib/ModelTheory/Basic.lean
Modified
Mathlib/ModelTheory/Complexity.lean
Modified
Mathlib/ModelTheory/Definability.lean
Modified
Mathlib/ModelTheory/DirectLimit.lean
Modified
Mathlib/ModelTheory/ElementaryMaps.lean
Modified
Mathlib/ModelTheory/Fraisse.lean
Modified
Mathlib/ModelTheory/LanguageMap.lean
Modified
Mathlib/ModelTheory/Order.lean
Modified
Mathlib/ModelTheory/PartialEquiv.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/ModelTheory/Syntax.lean
Modified
Mathlib/ModelTheory/Types.lean
Modified
Mathlib/NumberTheory/ADEInequality.lean
Modified
Mathlib/NumberTheory/AbelSummation.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Misc.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/VonMangoldt.lean
Modified
Mathlib/NumberTheory/Basic.lean
Modified
Mathlib/NumberTheory/Bernoulli.lean
Modified
Mathlib/NumberTheory/BernoulliPolynomials.lean
Modified
Mathlib/NumberTheory/Bertrand.lean
Modified
Mathlib/NumberTheory/Chebyshev.lean
Modified
Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
Modified
Mathlib/NumberTheory/ClassNumber/Finite.lean
Modified
Mathlib/NumberTheory/ClassNumber/FunctionField.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Basic.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
Modified
Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
Modified
Mathlib/NumberTheory/Dioph.lean
Modified
Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
Modified
Mathlib/NumberTheory/Divisors.lean
Modified
Mathlib/NumberTheory/FLT/Basic.lean
Modified
Mathlib/NumberTheory/FLT/Three.lean
Modified
Mathlib/NumberTheory/FactorisationProperties.lean
Modified
Mathlib/NumberTheory/Fermat.lean
Modified
Mathlib/NumberTheory/FermatPsp.lean
Modified
Mathlib/NumberTheory/FunctionField.lean
Modified
Mathlib/NumberTheory/GaussSum.lean
Modified
Mathlib/NumberTheory/Harmonic/Bounds.lean
Modified
Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
Modified
Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
Modified
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
Modified
Mathlib/NumberTheory/Height/Basic.lean
Modified
Mathlib/NumberTheory/Height/NumberField.lean
Modified
Mathlib/NumberTheory/KummerDedekind.lean
Modified
Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
Modified
Mathlib/NumberTheory/LSeries/Basic.lean
Modified
Mathlib/NumberTheory/LSeries/Convergence.lean
Modified
Mathlib/NumberTheory/LSeries/Convolution.lean
Modified
Mathlib/NumberTheory/LSeries/Deriv.lean
Modified
Mathlib/NumberTheory/LSeries/Dirichlet.lean
Modified
Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
Modified
Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
Modified
Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
Modified
Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
Modified
Mathlib/NumberTheory/LSeries/Linearity.lean
Modified
Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
Modified
Mathlib/NumberTheory/LSeries/Nonvanishing.lean
deleted
def
DirichletCharacter.zetaMul
Modified
Mathlib/NumberTheory/LSeries/PrimesInAP.lean
Modified
Mathlib/NumberTheory/LSeries/SumCoeff.lean
Modified
Mathlib/NumberTheory/LSeries/ZMod.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/Basic.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
Modified
Mathlib/NumberTheory/LocalField/Basic.lean
Modified
Mathlib/NumberTheory/LucasLehmer.lean
Modified
Mathlib/NumberTheory/MahlerMeasure.lean
Modified
Mathlib/NumberTheory/MaricaSchoenheim.lean
Modified
Mathlib/NumberTheory/Modular.lean
Modified
Mathlib/NumberTheory/ModularForms/Basic.lean
Modified
Mathlib/NumberTheory/ModularForms/BoundedAtCusp.lean
Modified
Mathlib/NumberTheory/ModularForms/Bounds.lean
Modified
Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
Modified
Mathlib/NumberTheory/ModularForms/Cusps.lean
deleted
def
cusps_subMulAction
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
Modified
Mathlib/NumberTheory/ModularForms/Identities.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
Modified
Mathlib/NumberTheory/ModularForms/LevelOne.lean
Modified
Mathlib/NumberTheory/ModularForms/NormTrace.lean
Modified
Mathlib/NumberTheory/ModularForms/Petersson.lean
Modified
Mathlib/NumberTheory/ModularForms/QExpansion.lean
Modified
Mathlib/NumberTheory/ModularForms/SlashActions.lean
Modified
Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean
Modified
Mathlib/NumberTheory/MulChar/Lemmas.lean
Modified
Mathlib/NumberTheory/Multiplicity.lean
Modified
Mathlib/NumberTheory/Niven.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/ConvexBody.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean
Modified
Mathlib/NumberTheory/NumberField/ClassNumber.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/PID.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Three.lean
Modified
Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean
Modified
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
Modified
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
Modified
Mathlib/NumberTheory/NumberField/FractionalIdeal.lean
Modified
Mathlib/NumberTheory/NumberField/House.lean
Modified
Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean
Modified
Mathlib/NumberTheory/NumberField/Ideal/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
Modified
Mathlib/NumberTheory/NumberField/Norm.lean
Modified
Mathlib/NumberTheory/NumberField/ProductFormula.lean
Modified
Mathlib/NumberTheory/NumberField/Units/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
Modified
Mathlib/NumberTheory/NumberField/Units/Regulator.lean
Modified
Mathlib/NumberTheory/Ostrowski.lean
Modified
Mathlib/NumberTheory/Padics/AddChar.lean
Modified
Mathlib/NumberTheory/Padics/Complex.lean
Modified
Mathlib/NumberTheory/Padics/Hensel.lean
Modified
Mathlib/NumberTheory/Padics/MahlerBasis.lean
Modified
Mathlib/NumberTheory/Padics/PadicIntegers.lean
Modified
Mathlib/NumberTheory/Padics/PadicNorm.lean
Modified
Mathlib/NumberTheory/Padics/PadicNumbers.lean
Modified
Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
Modified
Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
Modified
Mathlib/NumberTheory/Padics/ProperSpace.lean
Modified
Mathlib/NumberTheory/Padics/RingHoms.lean
Modified
Mathlib/NumberTheory/Padics/ValuativeRel.lean
Modified
Mathlib/NumberTheory/Padics/WithVal.lean
Modified
Mathlib/NumberTheory/Pell.lean
Modified
Mathlib/NumberTheory/PellMatiyasevic.lean
Modified
Mathlib/NumberTheory/Primorial.lean
Modified
Mathlib/NumberTheory/PythagoreanTriples.lean
Modified
Mathlib/NumberTheory/RamificationInertia/Basic.lean
Modified
Mathlib/NumberTheory/RamificationInertia/Galois.lean
Modified
Mathlib/NumberTheory/Rayleigh.lean
Modified
Mathlib/NumberTheory/Real/GoldenRatio.lean
Modified
Mathlib/NumberTheory/Real/Irrational.lean
Modified
Mathlib/NumberTheory/SiegelsLemma.lean
Modified
Mathlib/NumberTheory/SmoothNumbers.lean
Modified
Mathlib/NumberTheory/SumFourSquares.lean
Modified
Mathlib/NumberTheory/SumPrimeReciprocals.lean
Modified
Mathlib/NumberTheory/SumTwoSquares.lean
Modified
Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean
Modified
Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
Modified
Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
Modified
Mathlib/NumberTheory/TsumDivisorsAntidiagonal.lean
Modified
Mathlib/NumberTheory/WellApproximable.lean
Modified
Mathlib/NumberTheory/ZetaValues.lean
Modified
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
Modified
Mathlib/Order/Antisymmetrization.lean
Modified
Mathlib/Order/Atoms.lean
Modified
Mathlib/Order/Birkhoff.lean
Modified
Mathlib/Order/BooleanAlgebra/Set.lean
Modified
Mathlib/Order/BooleanGenerators.lean
Modified
Mathlib/Order/BooleanSubalgebra.lean
Modified
Mathlib/Order/Bounds/OrderIso.lean
Modified
Mathlib/Order/Category/BddDistLat.lean
Modified
Mathlib/Order/Category/BddLat.lean
Modified
Mathlib/Order/Category/BddOrd.lean
Modified
Mathlib/Order/Category/BoolAlg.lean
Modified
Mathlib/Order/Category/CompleteLat.lean
Modified
Mathlib/Order/Category/DistLat.lean
Modified
Mathlib/Order/Category/FinBddDistLat.lean
Modified
Mathlib/Order/Category/FinBoolAlg.lean
Modified
Mathlib/Order/Category/Frm.lean
Modified
Mathlib/Order/Category/HeytAlg.lean
Modified
Mathlib/Order/Category/Lat.lean
Modified
Mathlib/Order/Category/NonemptyFinLinOrd.lean
Modified
Mathlib/Order/Category/PartOrdEmb.lean
Modified
Mathlib/Order/Category/Semilat.lean
Modified
Mathlib/Order/CompactlyGenerated/Basic.lean
Modified
Mathlib/Order/CompleteLattice/Finset.lean
Modified
Mathlib/Order/CompleteLattice/PiLex.lean
Modified
Mathlib/Order/CompleteLattice/SetLike.lean
Modified
Mathlib/Order/CompleteLatticeIntervals.lean
Modified
Mathlib/Order/CompleteSublattice.lean
Modified
Mathlib/Order/Concept.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
Modified
Mathlib/Order/Copy.lean
Modified
Mathlib/Order/CountableDenseLinearOrder.lean
Modified
Mathlib/Order/Cover.lean
Modified
Mathlib/Order/Defs/LinearOrder.lean
Modified
Mathlib/Order/Defs/PartialOrder.lean
modified
theorem
le_refl
Modified
Mathlib/Order/Filter/AtTopBot/Finset.lean
Modified
Mathlib/Order/Filter/AtTopBot/Group.lean
Modified
Mathlib/Order/Filter/AtTopBot/Interval.lean
Modified
Mathlib/Order/Filter/AtTopBot/Tendsto.lean
Modified
Mathlib/Order/Filter/Bases/Basic.lean
Modified
Mathlib/Order/Filter/Basic.lean
Modified
Mathlib/Order/Filter/ENNReal.lean
Modified
Mathlib/Order/Filter/IsBounded.lean
Modified
Mathlib/Order/Filter/Map.lean
Modified
Mathlib/Order/Filter/Pointwise.lean
Modified
Mathlib/Order/Fin/Finset.lean
Modified
Mathlib/Order/Fin/SuccAboveOrderIso.lean
Modified
Mathlib/Order/Fin/Tuple.lean
Modified
Mathlib/Order/Height.lean
Modified
Mathlib/Order/Heyting/Regular.lean
Modified
Mathlib/Order/Hom/Basic.lean
Modified
Mathlib/Order/Hom/CompleteLattice.lean
Modified
Mathlib/Order/Hom/Lex.lean
Modified
Mathlib/Order/Hom/Set.lean
Modified
Mathlib/Order/Hom/WithTopBot.lean
Modified
Mathlib/Order/Interval/Basic.lean
Modified
Mathlib/Order/Interval/Finset/Basic.lean
Modified
Mathlib/Order/Interval/Finset/Defs.lean
Modified
Mathlib/Order/Interval/Finset/DenselyOrdered.lean
Modified
Mathlib/Order/Interval/Finset/Gaps.lean
Modified
Mathlib/Order/Interval/Set/Disjoint.lean
Modified
Mathlib/Order/Interval/Set/OrdConnected.lean
Modified
Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
Modified
Mathlib/Order/Interval/Set/Pi.lean
Modified
Mathlib/Order/Interval/Set/WithBotTop.lean
Modified
Mathlib/Order/JordanHolder.lean
Modified
Mathlib/Order/KrullDimension.lean
Modified
Mathlib/Order/Lattice/Congruence.lean
Modified
Mathlib/Order/LiminfLimsup.lean
Modified
Mathlib/Order/Minimal.lean
Modified
Mathlib/Order/Monotone/Extension.lean
Modified
Mathlib/Order/Monotone/Odd.lean
Modified
Mathlib/Order/OmegaCompletePartialOrder.lean
Modified
Mathlib/Order/Partition/Equipartition.lean
Modified
Mathlib/Order/Partition/Finpartition.lean
Modified
Mathlib/Order/PiLex.lean
Modified
Mathlib/Order/Preorder/Finsupp.lean
Modified
Mathlib/Order/PrimeSeparator.lean
Modified
Mathlib/Order/RelClasses.lean
added
theorem
Std.ge_refl
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/Order/Shrink.lean
Modified
Mathlib/Order/Sublattice.lean
Modified
Mathlib/Order/Sublocale.lean
Modified
Mathlib/Order/SuccPred/Archimedean.lean
Modified
Mathlib/Order/SuccPred/Basic.lean
Modified
Mathlib/Order/SuccPred/LinearLocallyFinite.lean
Modified
Mathlib/Order/SuccPred/Tree.lean
Modified
Mathlib/Order/SuccPred/WithBot.lean
Modified
Mathlib/Order/SupIndep.lean
Modified
Mathlib/Order/UpperLower/Closure.lean
Modified
Mathlib/Order/UpperLower/CompleteLattice.lean
Modified
Mathlib/Order/UpperLower/Relative.lean
Modified
Mathlib/Order/WellFounded.lean
Modified
Mathlib/Order/WellFoundedSet.lean
Modified
Mathlib/Order/WithBot.lean
Modified
Mathlib/Order/WithBotTop.lean
Modified
Mathlib/Probability/BorelCantelli.lean
Modified
Mathlib/Probability/ConditionalProbability.lean
Modified
Mathlib/Probability/Distributions/Beta.lean
Modified
Mathlib/Probability/Distributions/Cauchy.lean
Modified
Mathlib/Probability/Distributions/Exponential.lean
Modified
Mathlib/Probability/Distributions/Fernique.lean
Modified
Mathlib/Probability/Distributions/Gamma.lean
Modified
Mathlib/Probability/Distributions/Gaussian/Basic.lean
Modified
Mathlib/Probability/Distributions/Gaussian/CharFun.lean
Modified
Mathlib/Probability/Distributions/Gaussian/Fernique.lean
Modified
Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean
Modified
Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean
Modified
Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean
Modified
Mathlib/Probability/Distributions/Gaussian/Real.lean
Modified
Mathlib/Probability/Distributions/Pareto.lean
Modified
Mathlib/Probability/Distributions/SetBernoulli.lean
Modified
Mathlib/Probability/Distributions/Uniform.lean
Modified
Mathlib/Probability/IdentDistrib.lean
Modified
Mathlib/Probability/Independence/Basic.lean
Modified
Mathlib/Probability/Independence/BoundedContinuousFunction.lean
Modified
Mathlib/Probability/Independence/Kernel/IndepFun.lean
Modified
Mathlib/Probability/Independence/Process.lean
Modified
Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
Modified
Mathlib/Probability/Kernel/Disintegration/Density.lean
Modified
Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean
Modified
Mathlib/Probability/Kernel/Irreducible.lean
Modified
Mathlib/Probability/Kernel/Proper.lean
Modified
Mathlib/Probability/Kernel/RadonNikodym.lean
Modified
Mathlib/Probability/Kernel/WithDensity.lean
Modified
Mathlib/Probability/Martingale/Basic.lean
Modified
Mathlib/Probability/Martingale/BorelCantelli.lean
Modified
Mathlib/Probability/Martingale/OptionalSampling.lean
Modified
Mathlib/Probability/Martingale/OptionalStopping.lean
Modified
Mathlib/Probability/Martingale/Upcrossing.lean
Modified
Mathlib/Probability/Moments/Basic.lean
Modified
Mathlib/Probability/Moments/ComplexMGF.lean
Modified
Mathlib/Probability/Moments/CovarianceBilin.lean
Modified
Mathlib/Probability/Moments/CovarianceBilinDual.lean
Modified
Mathlib/Probability/Moments/IntegrableExpMul.lean
Modified
Mathlib/Probability/Moments/MGFAnalytic.lean
Modified
Mathlib/Probability/Moments/SubGaussian.lean
Modified
Mathlib/Probability/Moments/Variance.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
Modified
Mathlib/Probability/Process/Filtration.lean
Modified
Mathlib/Probability/Process/HittingTime.lean
Modified
Mathlib/Probability/Process/Predictable.lean
Modified
Mathlib/Probability/Process/Stopping.lean
Modified
Mathlib/Probability/ProductMeasure.lean
Modified
Mathlib/Probability/StrongLaw.lean
Modified
Mathlib/RepresentationTheory/Basic.lean
Modified
Mathlib/RepresentationTheory/Character.lean
Modified
Mathlib/RepresentationTheory/Coinduced.lean
Modified
Mathlib/RepresentationTheory/Coinvariants.lean
Modified
Mathlib/RepresentationTheory/FDRep.lean
Modified
Mathlib/RepresentationTheory/FinGroupCharZero.lean
Modified
Mathlib/RepresentationTheory/FiniteIndex.lean
Modified
Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.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/GroupHomology/Shapiro.lean
Modified
Mathlib/RepresentationTheory/Homological/Resolution.lean
Modified
Mathlib/RepresentationTheory/Induced.lean
Modified
Mathlib/RepresentationTheory/Intertwining.lean
deleted
def
Representation.IntertwiningMap.equivAlgEnd
Modified
Mathlib/RepresentationTheory/Invariants.lean
Modified
Mathlib/RepresentationTheory/Irreducible.lean
Modified
Mathlib/RepresentationTheory/Maschke.lean
Modified
Mathlib/RepresentationTheory/Rep.lean
Modified
Mathlib/RepresentationTheory/Semisimple.lean
Modified
Mathlib/RepresentationTheory/Subrepresentation.lean
Modified
Mathlib/RepresentationTheory/Tannaka.lean
Modified
Mathlib/RingTheory/AdicCompletion/Algebra.lean
Modified
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
Modified
Mathlib/RingTheory/AdicCompletion/Basic.lean
Modified
Mathlib/RingTheory/AdicCompletion/Exactness.lean
Modified
Mathlib/RingTheory/AdicCompletion/Functoriality.lean
Modified
Mathlib/RingTheory/AdicCompletion/LocalRing.lean
Modified
Mathlib/RingTheory/AdicCompletion/RingHom.lean
Modified
Mathlib/RingTheory/AdicCompletion/Topology.lean
Modified
Mathlib/RingTheory/Adjoin/Dimension.lean
Modified
Mathlib/RingTheory/Adjoin/Field.lean
Modified
Mathlib/RingTheory/Adjoin/PowerBasis.lean
Modified
Mathlib/RingTheory/Adjoin/Tower.lean
Modified
Mathlib/RingTheory/AdjoinRoot.lean
Modified
Mathlib/RingTheory/Algebraic/Basic.lean
Modified
Mathlib/RingTheory/Algebraic/Defs.lean
Modified
Mathlib/RingTheory/Algebraic/Integral.lean
Modified
Mathlib/RingTheory/Algebraic/MvPolynomial.lean
Modified
Mathlib/RingTheory/Algebraic/Pi.lean
Modified
Mathlib/RingTheory/Algebraic/StronglyTranscendental.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
Modified
Mathlib/RingTheory/Artinian/Algebra.lean
Modified
Mathlib/RingTheory/Artinian/Module.lean
Modified
Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
Modified
Mathlib/RingTheory/Bialgebra/TensorProduct.lean
Modified
Mathlib/RingTheory/Binomial.lean
Modified
Mathlib/RingTheory/ChainOfDivisors.lean
Modified
Mathlib/RingTheory/ClassGroup.lean
Modified
Mathlib/RingTheory/Coalgebra/Basic.lean
Modified
Mathlib/RingTheory/Coalgebra/Convolution.lean
Modified
Mathlib/RingTheory/Coalgebra/TensorProduct.lean
Modified
Mathlib/RingTheory/Complex.lean
Modified
Mathlib/RingTheory/Conductor.lean
Modified
Mathlib/RingTheory/Congruence/Hom.lean
Modified
Mathlib/RingTheory/Coprime/Lemmas.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DedekindDomain/Basic.lean
Modified
Mathlib/RingTheory/DedekindDomain/Different.lean
Modified
Mathlib/RingTheory/DedekindDomain/Dvr.lean
Modified
Mathlib/RingTheory/DedekindDomain/Factorization.lean
Modified
Mathlib/RingTheory/DedekindDomain/GaussLemma.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
Modified
Mathlib/RingTheory/DedekindDomain/Instances.lean
Modified
Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
Modified
Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean
Modified
Mathlib/RingTheory/Derivation/Basic.lean
Modified
Mathlib/RingTheory/Derivation/Lie.lean
Modified
Mathlib/RingTheory/Derivation/MapCoeffs.lean
Modified
Mathlib/RingTheory/Derivation/ToSquareZero.lean
Modified
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
Modified
Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
Modified
Mathlib/RingTheory/Discriminant.lean
Modified
Mathlib/RingTheory/DividedPowers/RatAlgebra.lean
Modified
Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean
Modified
Mathlib/RingTheory/EssentialFiniteness.lean
Modified
Mathlib/RingTheory/Etale/Field.lean
Modified
Mathlib/RingTheory/Etale/Kaehler.lean
Modified
Mathlib/RingTheory/Etale/QuasiFinite.lean
Modified
Mathlib/RingTheory/Etale/StandardEtale.lean
Modified
Mathlib/RingTheory/Extension/Basic.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/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/FiniteLength.lean
Modified
Mathlib/RingTheory/FinitePresentation.lean
Modified
Mathlib/RingTheory/FiniteStability.lean
Modified
Mathlib/RingTheory/FiniteType.lean
Modified
Mathlib/RingTheory/Finiteness/Basic.lean
Modified
Mathlib/RingTheory/Finiteness/Descent.lean
Modified
Mathlib/RingTheory/Finiteness/Finsupp.lean
Modified
Mathlib/RingTheory/Finiteness/NilpotentKer.lean
Modified
Mathlib/RingTheory/Fintype.lean
Modified
Mathlib/RingTheory/Flat/Basic.lean
Modified
Mathlib/RingTheory/Flat/Equalizer.lean
Modified
Mathlib/RingTheory/Flat/EquationalCriterion.lean
Modified
Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
Modified
Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
Modified
Mathlib/RingTheory/Flat/Tensor.lean
Modified
Mathlib/RingTheory/FractionalIdeal/Basic.lean
Modified
Mathlib/RingTheory/FractionalIdeal/Norm.lean
Modified
Mathlib/RingTheory/FractionalIdeal/Operations.lean
Modified
Mathlib/RingTheory/FreeCommRing.lean
Modified
Mathlib/RingTheory/Frobenius.lean
Modified
Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
Modified
Mathlib/RingTheory/GradedAlgebra/Homogeneous/Subsemiring.lean
Modified
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
Modified
Mathlib/RingTheory/HahnSeries/Addition.lean
Modified
Mathlib/RingTheory/HahnSeries/Basic.lean
Modified
Mathlib/RingTheory/HahnSeries/Binomial.lean
Modified
Mathlib/RingTheory/HahnSeries/HEval.lean
Modified
Mathlib/RingTheory/HahnSeries/HahnEmbedding.lean
Modified
Mathlib/RingTheory/HahnSeries/Lex.lean
Modified
Mathlib/RingTheory/HahnSeries/Multiplication.lean
Modified
Mathlib/RingTheory/HahnSeries/PowerSeries.lean
Modified
Mathlib/RingTheory/HahnSeries/Summable.lean
Modified
Mathlib/RingTheory/HopfAlgebra/Basic.lean
Modified
Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean
Modified
Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean
Modified
Mathlib/RingTheory/HopkinsLevitzki.lean
Modified
Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
Modified
Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean
Modified
Mathlib/RingTheory/Ideal/Cotangent.lean
Modified
Mathlib/RingTheory/Ideal/GoingUp.lean
Modified
Mathlib/RingTheory/Ideal/Height.lean
Modified
Mathlib/RingTheory/Ideal/Int.lean
Modified
Mathlib/RingTheory/Ideal/IsPrincipal.lean
Modified
Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean
Modified
Mathlib/RingTheory/Ideal/Maximal.lean
Modified
Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
Modified
Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
Modified
Mathlib/RingTheory/Ideal/Over.lean
Modified
Mathlib/RingTheory/Ideal/Pointwise.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/Defs.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Index.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Operations.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean
Modified
Mathlib/RingTheory/Idempotents.lean
Modified
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
Modified
Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean
Modified
Mathlib/RingTheory/IntegralClosure/GoingDown.lean
Modified
Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
Modified
Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
Modified
Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean
Modified
Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.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/Jacobson/Radical.lean
Modified
Mathlib/RingTheory/Jacobson/Ring.lean
Modified
Mathlib/RingTheory/Jacobson/Semiprimary.lean
Modified
Mathlib/RingTheory/Kaehler/Basic.lean
Modified
Mathlib/RingTheory/Kaehler/JacobiZariski.lean
Modified
Mathlib/RingTheory/Kaehler/Polynomial.lean
Modified
Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean
Modified
Mathlib/RingTheory/KrullDimension/Polynomial.lean
Modified
Mathlib/RingTheory/KrullDimension/Zero.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/Length.lean
Modified
Mathlib/RingTheory/LinearDisjoint.lean
Modified
Mathlib/RingTheory/LittleWedderburn.lean
Modified
Mathlib/RingTheory/LocalProperties/Basic.lean
Modified
Mathlib/RingTheory/LocalProperties/Exactness.lean
Modified
Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean
Modified
Mathlib/RingTheory/LocalProperties/Projective.lean
Modified
Mathlib/RingTheory/LocalRing/Module.lean
Modified
Mathlib/RingTheory/LocalRing/Quotient.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean
Modified
Mathlib/RingTheory/Localization/AsSubring.lean
Modified
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
Modified
Mathlib/RingTheory/Localization/AtPrime/Extension.lean
Modified
Mathlib/RingTheory/Localization/BaseChange.lean
Modified
Mathlib/RingTheory/Localization/Basic.lean
Modified
Mathlib/RingTheory/Localization/Defs.lean
Modified
Mathlib/RingTheory/Localization/FractionRing.lean
Modified
Mathlib/RingTheory/Localization/Ideal.lean
Modified
Mathlib/RingTheory/Localization/Integral.lean
Modified
Mathlib/RingTheory/Localization/Submodule.lean
Modified
Mathlib/RingTheory/MatrixAlgebra.lean
Modified
Mathlib/RingTheory/MatrixPolynomialAlgebra.lean
Modified
Mathlib/RingTheory/Morita/Matrix.lean
Modified
Mathlib/RingTheory/Multiplicity.lean
Modified
Mathlib/RingTheory/MvPolynomial.lean
Modified
Mathlib/RingTheory/MvPolynomial/Basic.lean
Modified
Mathlib/RingTheory/MvPolynomial/EulerIdentity.lean
Modified
Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean
Modified
Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
Modified
Mathlib/RingTheory/MvPolynomial/Ideal.lean
Modified
Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean
Modified
Mathlib/RingTheory/MvPolynomial/Localization.lean
Modified
Mathlib/RingTheory/MvPolynomial/MonomialOrder.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/LexOrder.lean
Modified
Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
Modified
Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Substitution.lean
Modified
Mathlib/RingTheory/Nakayama.lean
Modified
Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean
Modified
Mathlib/RingTheory/NoetherNormalization.lean
Modified
Mathlib/RingTheory/Noetherian/Basic.lean
Modified
Mathlib/RingTheory/Noetherian/Orzech.lean
Modified
Mathlib/RingTheory/NonUnitalSubring/Basic.lean
Modified
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
Modified
Mathlib/RingTheory/Norm/Basic.lean
Modified
Mathlib/RingTheory/Norm/Transitivity.lean
Modified
Mathlib/RingTheory/NormalClosure.lean
Modified
Mathlib/RingTheory/Nullstellensatz.lean
Modified
Mathlib/RingTheory/OrderOfVanishing.lean
Modified
Mathlib/RingTheory/Perfection.lean
Modified
Mathlib/RingTheory/Perfectoid/FontaineTheta.lean
Modified
Mathlib/RingTheory/Perfectoid/Untilt.lean
Modified
Mathlib/RingTheory/PicardGroup.lean
Modified
Mathlib/RingTheory/Polynomial/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Bernstein.lean
Modified
Mathlib/RingTheory/Polynomial/Chebyshev.lean
Modified
Mathlib/RingTheory/Polynomial/ContentIdeal.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
Modified
Mathlib/RingTheory/Polynomial/DegreeLT.lean
Modified
Mathlib/RingTheory/Polynomial/Dickson.lean
Modified
Mathlib/RingTheory/Polynomial/Eisenstein/Criterion.lean
Modified
Mathlib/RingTheory/Polynomial/Eisenstein/Distinguished.lean
Modified
Mathlib/RingTheory/Polynomial/GaussLemma.lean
Modified
Mathlib/RingTheory/Polynomial/GaussNorm.lean
Modified
Mathlib/RingTheory/Polynomial/HilbertPoly.lean
Modified
Mathlib/RingTheory/Polynomial/IsIntegral.lean
Modified
Mathlib/RingTheory/Polynomial/Morse.lean
Modified
Mathlib/RingTheory/Polynomial/Nilpotent.lean
Modified
Mathlib/RingTheory/Polynomial/Opposites.lean
Modified
Mathlib/RingTheory/Polynomial/Pochhammer.lean
Modified
Mathlib/RingTheory/Polynomial/Quotient.lean
Modified
Mathlib/RingTheory/Polynomial/RationalRoot.lean
Modified
Mathlib/RingTheory/Polynomial/Resultant/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/ScaleRoots.lean
Modified
Mathlib/RingTheory/Polynomial/SeparableDegree.lean
Modified
Mathlib/RingTheory/Polynomial/ShiftedLegendre.lean
Modified
Mathlib/RingTheory/Polynomial/Tower.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/Basic.lean
Modified
Mathlib/RingTheory/PowerSeries/Binomial.lean
Modified
Mathlib/RingTheory/PowerSeries/Catalan.lean
Modified
Mathlib/RingTheory/PowerSeries/Derivative.lean
Modified
Mathlib/RingTheory/PowerSeries/Exp.lean
Modified
Mathlib/RingTheory/PowerSeries/Expand.lean
Modified
Mathlib/RingTheory/PowerSeries/Ideal.lean
Modified
Mathlib/RingTheory/PowerSeries/Inverse.lean
Modified
Mathlib/RingTheory/PowerSeries/NoZeroDivisors.lean
Modified
Mathlib/RingTheory/PowerSeries/Order.lean
Modified
Mathlib/RingTheory/PowerSeries/PiTopology.lean
Modified
Mathlib/RingTheory/PowerSeries/Restricted.lean
Modified
Mathlib/RingTheory/PowerSeries/Schroder.lean
Modified
Mathlib/RingTheory/PowerSeries/Substitution.lean
Modified
Mathlib/RingTheory/PowerSeries/Trunc.lean
Modified
Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean
Modified
Mathlib/RingTheory/PowerSeries/WellKnown.lean
Modified
Mathlib/RingTheory/QuasiFinite/Basic.lean
Modified
Mathlib/RingTheory/QuasiFinite/Polynomial.lean
Modified
Mathlib/RingTheory/QuasiFinite/Weakly.lean
Modified
Mathlib/RingTheory/ReesAlgebra.lean
Modified
Mathlib/RingTheory/Regular/Category.lean
Modified
Mathlib/RingTheory/Regular/IsSMulRegular.lean
Modified
Mathlib/RingTheory/Regular/RegularSequence.lean
Modified
Mathlib/RingTheory/RingHom/FinitePresentation.lean
Modified
Mathlib/RingTheory/RingHom/Flat.lean
Modified
Mathlib/RingTheory/RingHom/Locally.lean
Modified
Mathlib/RingTheory/RingHom/QuasiFinite.lean
Modified
Mathlib/RingTheory/RingHom/StandardSmooth.lean
Modified
Mathlib/RingTheory/RingHom/Unramified.lean
Modified
Mathlib/RingTheory/RingHomProperties.lean
Modified
Mathlib/RingTheory/RootsOfUnity/AlgebraicallyClosed.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Basic.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Complex.lean
Modified
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.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/Basic.lean
Modified
Mathlib/RingTheory/Smooth/Fiber.lean
Modified
Mathlib/RingTheory/Smooth/Field.lean
Modified
Mathlib/RingTheory/Smooth/Flat.lean
Modified
Mathlib/RingTheory/Smooth/IntegralClosure.lean
Modified
Mathlib/RingTheory/Smooth/Kaehler.lean
Modified
Mathlib/RingTheory/Smooth/Local.lean
Modified
Mathlib/RingTheory/Smooth/NoetherianDescent.lean
Modified
Mathlib/RingTheory/Smooth/Pi.lean
Modified
Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
Modified
Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/LTSeries.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Polynomial.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/Finite.lean
Modified
Mathlib/RingTheory/TensorProduct/Free.lean
Modified
Mathlib/RingTheory/TensorProduct/Maps.lean
Modified
Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean
Modified
Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
Modified
Mathlib/RingTheory/TensorProduct/Quotient.lean
Modified
Mathlib/RingTheory/Trace/Basic.lean
Modified
Mathlib/RingTheory/Trace/Defs.lean
Modified
Mathlib/RingTheory/Trace/Quotient.lean
Modified
Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/GCDMonoid.lean
Modified
Mathlib/RingTheory/Unramified/Basic.lean
Modified
Mathlib/RingTheory/Unramified/Field.lean
Modified
Mathlib/RingTheory/Unramified/LocalRing.lean
Modified
Mathlib/RingTheory/Unramified/LocalStructure.lean
Modified
Mathlib/RingTheory/Unramified/Locus.lean
Modified
Mathlib/RingTheory/Unramified/Pi.lean
Modified
Mathlib/RingTheory/Valuation/AlgebraInstances.lean
Modified
Mathlib/RingTheory/Valuation/Archimedean.lean
Modified
Mathlib/RingTheory/Valuation/Basic.lean
Modified
Mathlib/RingTheory/Valuation/Discrete/Basic.lean
Modified
Mathlib/RingTheory/Valuation/LocalSubring.lean
Modified
Mathlib/RingTheory/Valuation/RankOne.lean
Modified
Mathlib/RingTheory/Valuation/ValuationSubring.lean
Modified
Mathlib/RingTheory/WittVector/Basic.lean
Modified
Mathlib/RingTheory/WittVector/Defs.lean
Modified
Mathlib/RingTheory/WittVector/Frobenius.lean
Modified
Mathlib/RingTheory/WittVector/IsPoly.lean
Modified
Mathlib/RingTheory/WittVector/Isocrystal.lean
Modified
Mathlib/RingTheory/WittVector/StructurePolynomial.lean
Modified
Mathlib/RingTheory/WittVector/Teichmuller.lean
Modified
Mathlib/RingTheory/WittVector/WittPolynomial.lean
Modified
Mathlib/RingTheory/ZariskisMainTheorem.lean
Modified
Mathlib/SetTheory/Cardinal/Basic.lean
Modified
Mathlib/SetTheory/Cardinal/Embedding.lean
Modified
Mathlib/SetTheory/Cardinal/Finite.lean
Modified
Mathlib/SetTheory/Cardinal/Ordinal.lean
Modified
Mathlib/SetTheory/Cardinal/Subfield.lean
Modified
Mathlib/SetTheory/Game/Birthday.lean
Modified
Mathlib/SetTheory/Game/Nim.lean
Modified
Mathlib/SetTheory/Game/Ordinal.lean
Modified
Mathlib/SetTheory/Game/Short.lean
added
def
SetTheory.PGame.shortAdd
Modified
Mathlib/SetTheory/Lists.lean
added
def
Lists.Equiv.decidable
added
def
Lists.Subset.decidable
added
def
Lists.mem.decidable
Modified
Mathlib/SetTheory/Nimber/Basic.lean
Modified
Mathlib/SetTheory/Nimber/Field.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean
Modified
Mathlib/SetTheory/ZFC/Basic.lean
Modified
Mathlib/SetTheory/ZFC/Cardinal.lean
Modified
Mathlib/SetTheory/ZFC/Class.lean
Modified
Mathlib/SetTheory/ZFC/Ordinal.lean
Modified
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean
Modified
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Majorized.lean
Modified
Mathlib/Tactic/DeriveTraversable.lean
Modified
Mathlib/Tactic/FieldSimp/Lemmas.lean
Modified
Mathlib/Tactic/Linter/Multigoal.lean
Modified
Mathlib/Tactic/Module.lean
Modified
Mathlib/Tactic/NormNum/Abs.lean
Modified
Mathlib/Tactic/NormNum/Basic.lean
Modified
Mathlib/Tactic/NormNum/Eq.lean
Modified
Mathlib/Tactic/NormNum/GCD.lean
Modified
Mathlib/Tactic/NormNum/Ineq.lean
Modified
Mathlib/Tactic/NormNum/Inv.lean
Modified
Mathlib/Tactic/NormNum/Irrational.lean
Modified
Mathlib/Tactic/NormNum/LegendreSymbol.lean
Modified
Mathlib/Tactic/NormNum/NatSqrt.lean
Modified
Mathlib/Tactic/NormNum/Pow.lean
Modified
Mathlib/Tactic/NormNum/PowMod.lean
Modified
Mathlib/Tactic/NormNum/RealSqrt.lean
Modified
Mathlib/Tactic/NormNum/Result.lean
Modified
Mathlib/Tactic/Ring/Common.lean
Modified
Mathlib/Tactic/Translate/Core.lean
Modified
Mathlib/Tactic/Translate/UnfoldBoundary.lean
Modified
Mathlib/Topology/AlexandrovDiscrete.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/ConstMulAction.lean
Modified
Mathlib/Topology/Algebra/Constructions.lean
Modified
Mathlib/Topology/Algebra/FilterBasis.lean
Modified
Mathlib/Topology/Algebra/Group/GroupTopology.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/SummationFilter.lean
deleted
def
SummationFilter.comap
Modified
Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean
Modified
Mathlib/Topology/Algebra/IsUniformGroup/DiscreteSubgroup.lean
Modified
Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean
Modified
Mathlib/Topology/Algebra/Module/Basic.lean
Modified
Mathlib/Topology/Algebra/Module/Equiv.lean
Modified
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
Modified
Mathlib/Topology/Algebra/Module/LinearMap.lean
Modified
Mathlib/Topology/Algebra/Module/LocallyConvex.lean
Modified
Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
Modified
Mathlib/Topology/Algebra/Module/StrongTopology.lean
Modified
Mathlib/Topology/Algebra/Module/TransferInstance.lean
Modified
Mathlib/Topology/Algebra/Module/UniformConvergence.lean
Modified
Mathlib/Topology/Algebra/Module/WeakBilin.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
Modified
Mathlib/Topology/Algebra/Nonarchimedean/TotallyDisconnected.lean
Modified
Mathlib/Topology/Algebra/Order/Field.lean
Modified
Mathlib/Topology/Algebra/Polynomial.lean
Modified
Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean
Modified
Mathlib/Topology/Algebra/Ring/Real.lean
Modified
Mathlib/Topology/Algebra/StarSubalgebra.lean
Modified
Mathlib/Topology/Algebra/Support.lean
Modified
Mathlib/Topology/Algebra/UniformFilterBasis.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/ValuativeRel.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuedField.lean
Modified
Mathlib/Topology/Algebra/Valued/WithVal.lean
Modified
Mathlib/Topology/Bornology/Real.lean
Modified
Mathlib/Topology/CWComplex/Classical/Basic.lean
Modified
Mathlib/Topology/CWComplex/Classical/Finite.lean
Modified
Mathlib/Topology/CWComplex/Classical/Subcomplex.lean
Modified
Mathlib/Topology/Category/CompHaus/Basic.lean
Modified
Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean
Modified
Mathlib/Topology/Category/CompHausLike/Limits.lean
Modified
Mathlib/Topology/Category/CompHausLike/SigmaComparison.lean
Modified
Mathlib/Topology/Category/LightProfinite/AsLimit.lean
Modified
Mathlib/Topology/Category/LightProfinite/Basic.lean
Modified
Mathlib/Topology/Category/LightProfinite/Extend.lean
Modified
Mathlib/Topology/Category/LightProfinite/Injective.lean
Modified
Mathlib/Topology/Category/Profinite/AsLimit.lean
Modified
Mathlib/Topology/Category/Profinite/Basic.lean
Modified
Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
Modified
Mathlib/Topology/Category/Profinite/EffectiveEpi.lean
Modified
Mathlib/Topology/Category/Profinite/Extend.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/Stonean/Basic.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Basic.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Products.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
Modified
Mathlib/Topology/Category/TopCat/Opens.lean
Modified
Mathlib/Topology/Category/TopCat/Sphere.lean
Modified
Mathlib/Topology/Category/TopCat/ULift.lean
Modified
Mathlib/Topology/Category/TopCat/Yoneda.lean
Modified
Mathlib/Topology/Category/UniformSpace.lean
deleted
def
UniformSpaceCat.completionHom
Modified
Mathlib/Topology/Closure.lean
Modified
Mathlib/Topology/CompactOpen.lean
Modified
Mathlib/Topology/Compactification/OnePoint/Basic.lean
Modified
Mathlib/Topology/Compactification/OnePoint/Sphere.lean
Modified
Mathlib/Topology/Compactification/StoneCech.lean
Modified
Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
Modified
Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
Modified
Mathlib/Topology/Connected/Basic.lean
Modified
Mathlib/Topology/Connected/Clopen.lean
Modified
Mathlib/Topology/Connected/LocPathConnected.lean
Modified
Mathlib/Topology/Connected/PathConnected.lean
Modified
Mathlib/Topology/Constructible.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/ContinuousMap/Algebra.lean
Modified
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
Modified
Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
Modified
Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean
Modified
Mathlib/Topology/ContinuousMap/Compact.lean
Modified
Mathlib/Topology/ContinuousMap/CompactlySupported.lean
Modified
Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
Modified
Mathlib/Topology/ContinuousMap/Ideals.lean
Modified
Mathlib/Topology/ContinuousMap/Interval.lean
Modified
Mathlib/Topology/ContinuousMap/StarOrdered.lean
Modified
Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
Modified
Mathlib/Topology/ContinuousMap/T0Sierpinski.lean
Modified
Mathlib/Topology/ContinuousMap/Weierstrass.lean
Modified
Mathlib/Topology/Convenient/GeneratedBy.lean
Modified
Mathlib/Topology/Covering/AddCircle.lean
Modified
Mathlib/Topology/Defs/Filter.lean
Modified
Mathlib/Topology/DiscreteSubset.lean
Modified
Mathlib/Topology/EMetricSpace/Defs.lean
Modified
Mathlib/Topology/EMetricSpace/Lipschitz.lean
Modified
Mathlib/Topology/EMetricSpace/PairReduction.lean
Modified
Mathlib/Topology/EMetricSpace/Pi.lean
Modified
Mathlib/Topology/ExtremallyDisconnected.lean
Modified
Mathlib/Topology/FiberBundle/Basic.lean
Modified
Mathlib/Topology/GDelta/Basic.lean
Modified
Mathlib/Topology/Gluing.lean
Modified
Mathlib/Topology/Homotopy/Basic.lean
Modified
Mathlib/Topology/Homotopy/HSpaces.lean
Modified
Mathlib/Topology/Homotopy/HomotopyGroup.lean
Modified
Mathlib/Topology/Homotopy/Path.lean
Modified
Mathlib/Topology/IndicatorConstPointwise.lean
Modified
Mathlib/Topology/Instances/AddCircle/Defs.lean
Modified
Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean
Modified
Mathlib/Topology/Instances/CantorSet.lean
Modified
Mathlib/Topology/Instances/Complex.lean
Modified
Mathlib/Topology/Instances/Discrete.lean
Modified
Mathlib/Topology/Instances/ENNReal/Lemmas.lean
Modified
Mathlib/Topology/Instances/EReal/Lemmas.lean
Modified
Mathlib/Topology/Instances/Int.lean
Modified
Mathlib/Topology/Instances/Matrix.lean
Modified
Mathlib/Topology/Instances/NNReal/Lemmas.lean
Modified
Mathlib/Topology/Instances/Rat.lean
Modified
Mathlib/Topology/Instances/Real/Lemmas.lean
Modified
Mathlib/Topology/Instances/ZMultiples.lean
Modified
Mathlib/Topology/Irreducible.lean
Modified
Mathlib/Topology/IsClosedRestrict.lean
Modified
Mathlib/Topology/JacobsonSpace.lean
Modified
Mathlib/Topology/List.lean
Modified
Mathlib/Topology/LocalAtTarget.lean
Modified
Mathlib/Topology/MetricSpace/Basic.lean
Modified
Mathlib/Topology/MetricSpace/CantorScheme.lean
Modified
Mathlib/Topology/MetricSpace/Closeds.lean
Modified
Mathlib/Topology/MetricSpace/Contracting.lean
Modified
Mathlib/Topology/MetricSpace/CoveringNumbers.lean
Modified
Mathlib/Topology/MetricSpace/Dilation.lean
Modified
Mathlib/Topology/MetricSpace/Gluing.lean
Modified
Mathlib/Topology/MetricSpace/GromovHausdorff.lean
Modified
Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
Modified
Mathlib/Topology/MetricSpace/HausdorffDimension.lean
Modified
Mathlib/Topology/MetricSpace/HausdorffDistance.lean
Modified
Mathlib/Topology/MetricSpace/Holder.lean
Modified
Mathlib/Topology/MetricSpace/Infsep.lean
Modified
Mathlib/Topology/MetricSpace/Lipschitz.lean
Modified
Mathlib/Topology/MetricSpace/PiNat.lean
Modified
Mathlib/Topology/MetricSpace/Polish.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
Modified
Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
Modified
Mathlib/Topology/MetricSpace/Thickening.lean
Modified
Mathlib/Topology/MetricSpace/Ultra/Basic.lean
Modified
Mathlib/Topology/Metrizable/CompletelyMetrizable.lean
Modified
Mathlib/Topology/Metrizable/Uniformity.lean
Modified
Mathlib/Topology/Metrizable/Urysohn.lean
Modified
Mathlib/Topology/NatEmbedding.lean
Modified
Mathlib/Topology/NoetherianSpace.lean
Modified
Mathlib/Topology/OpenPartialHomeomorph/Basic.lean
Modified
Mathlib/Topology/Order.lean
Modified
Mathlib/Topology/Order/Basic.lean
Modified
Mathlib/Topology/Order/Bornology.lean
Modified
Mathlib/Topology/Order/Category/FrameAdjunction.lean
Modified
Mathlib/Topology/Order/HullKernel.lean
Modified
Mathlib/Topology/Order/IsLUB.lean
Modified
Mathlib/Topology/Order/Lattice.lean
Modified
Mathlib/Topology/Order/LawsonTopology.lean
Modified
Mathlib/Topology/Order/LeftRightLim.lean
Modified
Mathlib/Topology/Order/LeftRightNhds.lean
Modified
Mathlib/Topology/Order/LiminfLimsup.lean
Modified
Mathlib/Topology/Order/LocalExtr.lean
Modified
Mathlib/Topology/Order/LowerUpperTopology.lean
Modified
Mathlib/Topology/Order/Monotone.lean
Modified
Mathlib/Topology/Order/ScottTopology.lean
Modified
Mathlib/Topology/Order/T5.lean
Modified
Mathlib/Topology/Order/UpperLowerSetTopology.lean
Modified
Mathlib/Topology/Order/WithTop.lean
Modified
Mathlib/Topology/Path.lean
Modified
Mathlib/Topology/Semicontinuity/Defs.lean
Modified
Mathlib/Topology/Separation/Basic.lean
Modified
Mathlib/Topology/Separation/CompletelyRegular.lean
Modified
Mathlib/Topology/Separation/DisjointCover.lean
Modified
Mathlib/Topology/Separation/Hausdorff.lean
Modified
Mathlib/Topology/Separation/LinearUpperLowerSetTopology.lean
Modified
Mathlib/Topology/Separation/Regular.lean
Modified
Mathlib/Topology/Separation/SeparatedNhds.lean
Modified
Mathlib/Topology/Sets/Closeds.lean
Modified
Mathlib/Topology/Sets/CompactOpenCovered.lean
Modified
Mathlib/Topology/Sets/OpenCover.lean
Modified
Mathlib/Topology/Sets/Opens.lean
Modified
Mathlib/Topology/Sets/VietorisTopology.lean
Modified
Mathlib/Topology/Sheaves/Alexandrov.lean
Modified
Mathlib/Topology/Sheaves/CommRingCat.lean
Modified
Mathlib/Topology/Sheaves/Limits.lean
Modified
Mathlib/Topology/Sheaves/LocallySurjective.lean
Modified
Mathlib/Topology/Sheaves/MayerVietoris.lean
Modified
Mathlib/Topology/Sheaves/PUnit.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
Modified
Mathlib/Topology/Sheaves/Skyscraper.lean
Modified
Mathlib/Topology/Sheaves/Stalks.lean
Modified
Mathlib/Topology/Sober.lean
Modified
Mathlib/Topology/Spectral/Prespectral.lean
Modified
Mathlib/Topology/Subpath.lean
Modified
Mathlib/Topology/TietzeExtension.lean
Modified
Mathlib/Topology/UniformSpace/Ascoli.lean
Modified
Mathlib/Topology/UniformSpace/Basic.lean
Modified
Mathlib/Topology/UniformSpace/Cauchy.lean
Modified
Mathlib/Topology/UniformSpace/Closeds.lean
Modified
Mathlib/Topology/UniformSpace/CompareReals.lean
Modified
Mathlib/Topology/UniformSpace/Completion.lean
Modified
Mathlib/Topology/UniformSpace/Dini.lean
Modified
Mathlib/Topology/UniformSpace/Equicontinuity.lean
Modified
Mathlib/Topology/UniformSpace/OfCompactT2.lean
Modified
Mathlib/Topology/UniformSpace/Pi.lean
Modified
Mathlib/Topology/UniformSpace/Separation.lean
Modified
Mathlib/Topology/UniformSpace/Ultra/Constructions.lean
Modified
Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
Modified
Mathlib/Topology/UniformSpace/Uniformizable.lean
Modified
Mathlib/Topology/UnitInterval.lean
Modified
Mathlib/Topology/UrysohnsLemma.lean
Modified
Mathlib/Topology/VectorBundle/Basic.lean
Modified
Mathlib/Topology/VectorBundle/Riemannian.lean
Modified
MathlibTest/Algebra/Category/Grp/Injective.lean
Modified
MathlibTest/Algebra/Module/LocalizedModule.lean
Modified
MathlibTest/Bound/bound.lean
Modified
MathlibTest/CategoryTheory/CheckCompositions.lean
Modified
MathlibTest/FieldSimp.lean
Modified
MathlibTest/FindSyntax.lean
Modified
MathlibTest/GCongr/inequalities.lean
Modified
MathlibTest/LintStyle.lean
Modified
MathlibTest/Quaternion.lean
Modified
MathlibTest/Simps.lean
modified
def
coercing.bar
modified
def
coercing.new_bar
Modified
MathlibTest/TCSynth.lean
Modified
MathlibTest/TacticAnalysis.lean
Modified
MathlibTest/TautoSet.lean
Modified
MathlibTest/ToDual.lean
Modified
MathlibTest/cancel_denoms.lean
Modified
MathlibTest/congr.lean
Modified
MathlibTest/depRewrite.lean
Modified
MathlibTest/fast_instance.lean
Modified
MathlibTest/fun_prop2.lean
Modified
MathlibTest/globalAttributeIn.lean
Modified
MathlibTest/hintAll.lean
Modified
MathlibTest/instance_diamonds.lean
Modified
MathlibTest/instance_diamonds/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
Modified
MathlibTest/instance_diamonds/FieldTheory/SplittingField/Construction.lean
Modified
MathlibTest/linarith.lean
Modified
MathlibTest/linear_combination'.lean
Modified
MathlibTest/linear_combination.lean
Modified
MathlibTest/matrix.lean
Modified
MathlibTest/norm_num.lean
Modified
MathlibTest/push.lean
Modified
MathlibTest/reduce_mod_char.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
scripts/nolints.json
Modified
scripts/noshake.json