[Merged by Bors] - feat: more lemmas about torsion-free monoids by YaelDillies · Pull Request #24312 · leanprover-community/mathlib4

YaelDillies · 2025-04-23T11:47:06Z

The new imports just come from making #min_imports and mk_iff available earlier.

From Toric

github-actions · 2025-04-23T11:48:06Z

PR summary f84d401cbc

Import changes exceeding 2%

%	File
+4.50%	`Mathlib.Algebra.Group.Prod`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Prod	200	209	+9 (+4.50%)
Mathlib.Algebra.NoZeroSMulDivisors.Defs	195	196	+1 (+0.51%)
Mathlib.Algebra.Group.Pi.Lemmas	266	267	+1 (+0.38%)
Mathlib.Algebra.Group.Subgroup.Basic	435	436	+1 (+0.23%)
Mathlib.Topology.Instances.ZMultiples	1199	1197	-2 (-0.17%)
Mathlib.GroupTheory.OrderOfElement	890	891	+1 (+0.11%)
Mathlib.GroupTheory.Torsion	1109	1110	+1 (+0.09%)
Mathlib.Algebra.Lie.Weights.Chain	2023	2022	-1 (-0.05%)

Import changes for all files

Files	Import difference
7 files `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Topology.Instances.AddCircle` `Mathlib.Topology.Instances.ZMultiples`	-2
80 files `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Central.TensorProduct` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.CartanSubalgebra` `Mathlib.Algebra.Lie.Character` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.Semisimple.Basic` `Mathlib.Algebra.Lie.Semisimple.Defs` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `Mathlib.Algebra.Lie.Solvable` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.LinearAlgebra.LinearDisjoint` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Flat.Basic` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.RingTheory.Flat.Domain` `Mathlib.RingTheory.Flat.Equalizer` `Mathlib.RingTheory.Flat.EquationalCriterion` `Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra` `Mathlib.RingTheory.Flat.FaithfullyFlat.Basic` `Mathlib.RingTheory.Flat.Localization` `Mathlib.RingTheory.Flat.Stability` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Ideal.GoingDown` `Mathlib.RingTheory.LinearDisjoint` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.RingTheory.Regular.RegularSequence` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Spectrum.Prime.Chevalley` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.Homeomorph` `Mathlib.RingTheory.TensorProduct.Nontrivial` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.Topology.Instances.AddCircle.DenseSubgroup`	-1
2799 files `Mathlib.Algebra.AddTorsor.Basic` `Mathlib.Algebra.Algebra.Basic` `Mathlib.Algebra.Algebra.Bilinear` `Mathlib.Algebra.Algebra.Equiv` `Mathlib.Algebra.Algebra.Field` `Mathlib.Algebra.Algebra.Hom.Rat` `Mathlib.Algebra.Algebra.Hom` `Mathlib.Algebra.Algebra.NonUnitalHom` `Mathlib.Algebra.Algebra.NonUnitalSubalgebra` `Mathlib.Algebra.Algebra.Operations` `Mathlib.Algebra.Algebra.Opposite` `Mathlib.Algebra.Algebra.Pi` `Mathlib.Algebra.Algebra.Prod` `Mathlib.Algebra.Algebra.Rat` `Mathlib.Algebra.Algebra.RestrictScalars` `Mathlib.Algebra.Algebra.Spectrum.Basic` `Mathlib.Algebra.Algebra.Spectrum.Pi` `Mathlib.Algebra.Algebra.Spectrum.Quasispectrum` `Mathlib.Algebra.Algebra.Subalgebra.Basic` `Mathlib.Algebra.Algebra.Subalgebra.Centralizer` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder` `Mathlib.Algebra.Algebra.Subalgebra.Lattice` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.Algebra.Algebra.Subalgebra.Order` `Mathlib.Algebra.Algebra.Subalgebra.Pi` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Algebra.Algebra.Subalgebra.Rank` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.Algebra.Algebra.Tower` `Mathlib.Algebra.Algebra.Unitization` `Mathlib.Algebra.Algebra.ZMod` `Mathlib.Algebra.AlgebraicCard` `Mathlib.Algebra.Azumaya.Basic` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.Azumaya.Matrix` `Mathlib.Algebra.BigOperators.Associated` `Mathlib.Algebra.BigOperators.Balance` `Mathlib.Algebra.BigOperators.Expect` `Mathlib.Algebra.BigOperators.Field` `Mathlib.Algebra.BigOperators.Fin` `Mathlib.Algebra.BigOperators.Finprod` `Mathlib.Algebra.BigOperators.Finsupp.Basic` `Mathlib.Algebra.BigOperators.Finsupp.Fin` `Mathlib.Algebra.BigOperators.Group.Finset.Basic` `Mathlib.Algebra.BigOperators.Group.Finset.Defs` `Mathlib.Algebra.BigOperators.Group.Finset.Indicator` `Mathlib.Algebra.BigOperators.Group.Finset.Lemmas` `Mathlib.Algebra.BigOperators.Group.Finset.Pi` `Mathlib.Algebra.BigOperators.Group.Finset.Piecewise` `Mathlib.Algebra.BigOperators.Group.Finset.Powerset` `Mathlib.Algebra.BigOperators.Group.Finset.Preimage` `Mathlib.Algebra.BigOperators.Group.Finset.Sigma` `Mathlib.Algebra.BigOperators.Group.Multiset.Basic` `Mathlib.Algebra.BigOperators.GroupWithZero.Action` `Mathlib.Algebra.BigOperators.GroupWithZero.Finset` `Mathlib.Algebra.BigOperators.Intervals` `Mathlib.Algebra.BigOperators.Module` `Mathlib.Algebra.BigOperators.NatAntidiagonal` `Mathlib.Algebra.BigOperators.Option` `Mathlib.Algebra.BigOperators.Pi` `Mathlib.Algebra.BigOperators.Ring.Finset` `Mathlib.Algebra.BigOperators.Ring.Multiset` `Mathlib.Algebra.BigOperators.Ring.Nat` `Mathlib.Algebra.BigOperators.RingEquiv` `Mathlib.Algebra.BigOperators.Sym` `Mathlib.Algebra.BigOperators.WithTop` `Mathlib.Algebra.BrauerGroup.Defs` `Mathlib.Algebra.Category.AlgebraCat.Basic` `Mathlib.Algebra.Category.AlgebraCat.Limits` `Mathlib.Algebra.Category.AlgebraCat.Monoidal` `Mathlib.Algebra.Category.AlgebraCat.Symmetric` `Mathlib.Algebra.Category.BialgebraCat.Basic` `Mathlib.Algebra.Category.BialgebraCat.Monoidal` `Mathlib.Algebra.Category.BoolRing` `Mathlib.Algebra.Category.CoalgebraCat.Basic` `Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgebraCat.Monoidal` `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.Category.Grp.Adjunctions` `Mathlib.Algebra.Category.Grp.Basic` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.Algebra.Category.Grp.ChosenFiniteProducts` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Algebra.Category.Grp.EpiMono` `Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup` `Mathlib.Algebra.Category.Grp.FilteredColimits` `Mathlib.Algebra.Category.Grp.FiniteGrp` `Mathlib.Algebra.Category.Grp.ForgetCorepresentable` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Category.Grp.IsFinite` `Mathlib.Algebra.Category.Grp.Kernels` `Mathlib.Algebra.Category.Grp.LeftExactFunctor` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Algebra.Category.Grp.Preadditive` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.Grp.ZModuleEquivalence` `Mathlib.Algebra.Category.Grp.Zero` `Mathlib.Algebra.Category.HopfAlgebraCat.Basic` `Mathlib.Algebra.Category.HopfAlgebraCat.Monoidal` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.Algebra.Category.ModuleCat.Basic` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.Algebra.Category.ModuleCat.ExteriorPower` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Algebra.Category.ModuleCat.Pseudofunctor` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.Algebra.Category.ModuleCat.Tannaka` `Mathlib.Algebra.Category.MonCat.Adjunctions` `Mathlib.Algebra.Category.MonCat.FilteredColimits` `Mathlib.Algebra.Category.MonCat.Limits` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Category.Ring.Basic` `Mathlib.Algebra.Category.Ring.Colimits` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Category.Ring.FilteredColimits` `Mathlib.Algebra.Category.Ring.FinitePresentation` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.Central.Basic` `Mathlib.Algebra.Central.Defs` `Mathlib.Algebra.Central.Matrix` `Mathlib.Algebra.CharP.Algebra` `Mathlib.Algebra.CharP.Basic` `Mathlib.Algebra.CharP.CharAndCard` `Mathlib.Algebra.CharP.Frobenius` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Algebra.CharP.Lemmas` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Algebra.CharP.Pi` `Mathlib.Algebra.CharP.Quotient` `Mathlib.Algebra.CharP.Reduced` `Mathlib.Algebra.CharP.Subring` `Mathlib.Algebra.CharP.Two` `Mathlib.Algebra.CharZero.Quotient` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.Algebra.Colimit.Module` `Mathlib.Algebra.Colimit.Ring` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.ContinuedFractions.Computation.Approximations` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Algebra.DirectSum.AddChar` `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.Algebra.DirectSum.Basic` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.Algebra.DirectSum.Idempotents` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Algebra.DirectSum.LinearMap` `Mathlib.Algebra.DirectSum.Module` `Mathlib.Algebra.DirectSum.Ring` `Mathlib.Algebra.Divisibility.Prod` `Mathlib.Algebra.DualNumber` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.Equiv.TransferInstance` `Mathlib.Algebra.Exact` `Mathlib.Algebra.Field.Action.ConjAct` `Mathlib.Algebra.Field.NegOnePow` `Mathlib.Algebra.Field.Subfield.Basic` `Mathlib.Algebra.Field.ZMod` `Mathlib.Algebra.FiveLemma` `Mathlib.Algebra.FreeAbelianGroup.Finsupp` `Mathlib.Algebra.FreeAbelianGroup.UniqueSums` `Mathlib.Algebra.FreeAlgebra.Cardinality` `Mathlib.Algebra.FreeAlgebra` `Mathlib.Algebra.FreeMonoid.UniqueProds` `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.GeomSum` `Mathlib.Algebra.GradedMonoid` `Mathlib.Algebra.GradedMulAction` `Mathlib.Algebra.Group.Action.End` `Mathlib.Algebra.Group.Action.Equidecomp` `Mathlib.Algebra.Group.Action.Pointwise.Finset` `Mathlib.Algebra.Group.Action.Pointwise.Set.Finite` `Mathlib.Algebra.Group.AddChar` `Mathlib.Algebra.Group.ConjFinite` `Mathlib.Algebra.Group.Conj` `Mathlib.Algebra.Group.End` `Mathlib.Algebra.Group.EvenFunction` `Mathlib.Algebra.Group.ForwardDiff` `Mathlib.Algebra.Group.Graph` `Mathlib.Algebra.Group.Indicator` `Mathlib.Algebra.Group.NatPowAssoc` `Mathlib.Algebra.Group.Pi.Lemmas` `Mathlib.Algebra.Group.Pointwise.Finset.Basic` `Mathlib.Algebra.Group.Pointwise.Finset.BigOperators` `Mathlib.Algebra.Group.Pointwise.Finset.Density` `Mathlib.Algebra.Group.Pointwise.Finset.Interval` `Mathlib.Algebra.Group.Pointwise.Finset.Scalar` `Mathlib.Algebra.Group.Pointwise.Set.BigOperators` `Mathlib.Algebra.Group.Pointwise.Set.Card` `Mathlib.Algebra.Group.Pointwise.Set.Finite` `Mathlib.Algebra.Group.Pointwise.Set.ListOfFn` `Mathlib.Algebra.Group.Subgroup.Actions` `Mathlib.Algebra.Group.Subgroup.Basic` `Mathlib.Algebra.Group.Subgroup.Finite` `Mathlib.Algebra.Group.Subgroup.Finsupp` `Mathlib.Algebra.Group.Subgroup.Ker` `Mathlib.Algebra.Group.Subgroup.Lattice` `Mathlib.Algebra.Group.Subgroup.Map` `Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas` `Mathlib.Algebra.Group.Subgroup.Order` `Mathlib.Algebra.Group.Subgroup.Pointwise` `Mathlib.Algebra.Group.Subgroup.ZPowers.Basic` `Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas` `Mathlib.Algebra.Group.Submonoid.BigOperators` `Mathlib.Algebra.Group.Submonoid.Finsupp` `Mathlib.Algebra.Group.Submonoid.Membership` `Mathlib.Algebra.Group.Submonoid.Pointwise` `Mathlib.Algebra.Group.Submonoid.Units` `Mathlib.Algebra.Group.Translate` `Mathlib.Algebra.Group.UniqueProds.Basic` `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.Algebra.GroupWithZero.Action.Basic` `Mathlib.Algebra.GroupWithZero.Action.Center` `Mathlib.Algebra.GroupWithZero.Action.ConjAct` `Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset` `Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set` `Mathlib.Algebra.GroupWithZero.Conj` `Mathlib.Algebra.GroupWithZero.Indicator` `Mathlib.Algebra.GroupWithZero.NonZeroDivisors` `Mathlib.Algebra.GroupWithZero.Pointwise.Finset` `Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card` `Mathlib.Algebra.GroupWithZero.Subgroup` `Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise` `Mathlib.Algebra.Homology.Additive` `Mathlib.Algebra.Homology.AlternatingConst` `Mathlib.Algebra.Homology.Augment` `Mathlib.Algebra.Homology.BifunctorAssociator` `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Algebra.Homology.Bifunctor` `Mathlib.Algebra.Homology.CommSq` `Mathlib.Algebra.Homology.ComplexShapeSigns` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass` `Mathlib.Algebra.Homology.DerivedCategory.Fractions` `Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Algebra.Homology.DifferentialObject` `Mathlib.Algebra.Homology.Double` `Mathlib.Algebra.Homology.Embedding.Boundary` `Mathlib.Algebra.Homology.Embedding.CochainComplex` `Mathlib.Algebra.Homology.Embedding.Connect` `Mathlib.Algebra.Homology.Embedding.ExtendHomology` `Mathlib.Algebra.Homology.Embedding.Extend` `Mathlib.Algebra.Homology.Embedding.HomEquiv` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.Algebra.Homology.Embedding.RestrictionHomology` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.Embedding.StupidTrunc` `Mathlib.Algebra.Homology.Embedding.TruncGEHomology` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Algebra.Homology.Embedding.TruncLEHomology` `Mathlib.Algebra.Homology.Embedding.TruncLE` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Algebra.Homology.Functor` `Mathlib.Algebra.Homology.GrothendieckAbelian` `Mathlib.Algebra.Homology.HomologicalBicomplex` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Homology.HomologicalComplexBiprod` `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.Algebra.Homology.HomologicalComplex` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplex` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCone` `Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated` `Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence` `Mathlib.Algebra.Homology.HomotopyCategory.Shift` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors` `Mathlib.Algebra.Homology.HomotopyCategory.Triangulated` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.Algebra.Homology.Linear` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.Monoidal` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Algebra.Homology.ShortComplex.Abelian` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Algebra.Homology.ShortComplex.Exact` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.ShortComplex.Homology` `Mathlib.Algebra.Homology.ShortComplex.Limits` `Mathlib.Algebra.Homology.ShortComplex.Linear` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Algebra.Homology.ShortComplex.Preadditive` `Mathlib.Algebra.Homology.ShortComplex.PreservesHomology` `Mathlib.Algebra.Homology.ShortComplex.QuasiIso` `Mathlib.Algebra.Homology.ShortComplex.Retract` `Mathlib.Algebra.Homology.ShortComplex.RightHomology` `Mathlib.Algebra.Homology.ShortComplex.ShortExact` `Mathlib.Algebra.Homology.ShortComplex.SnakeLemma` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.Algebra.Homology.Single` `Mathlib.Algebra.Homology.Square` `Mathlib.Algebra.Homology.TotalComplexShift` `Mathlib.Algebra.Homology.TotalComplexSymmetry` `Mathlib.Algebra.Homology.TotalComplex` `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.Basic` `Mathlib.Algebra.Lie.CartanMatrix` `Mathlib.Algebra.Lie.Classical` `Mathlib.Algebra.Lie.Derivation.AdjointAction` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Free` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Ideal` `Mathlib.Algebra.Lie.Matrix` `Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.SkewAdjoint` `Mathlib.Algebra.Lie.Sl2` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Algebra.LinearRecurrence` `Mathlib.Algebra.ModEq` `Mathlib.Algebra.Module.Basic` `Mathlib.Algebra.Module.BigOperators` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Module.Card` `Mathlib.Algebra.Module.Equiv.Basic` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Module.Hom` `Mathlib.Algebra.Module.Injective` `Mathlib.Algebra.Module.Lattice` `Mathlib.Algebra.Module.LinearMap.Basic` `Mathlib.Algebra.Module.LinearMap.End` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.Algebra.Module.LinearMap.Prod` `Mathlib.Algebra.Module.LinearMap.Rat` `Mathlib.Algebra.Module.LinearMap.Star` `Mathlib.Algebra.Module.LocalizedModule.AtPrime` `Mathlib.Algebra.Module.LocalizedModule.Away` `Mathlib.Algebra.Module.LocalizedModule.Basic` `Mathlib.Algebra.Module.LocalizedModule.Exact` `Mathlib.Algebra.Module.LocalizedModule.Int` `Mathlib.Algebra.Module.LocalizedModule.IsLocalization` `Mathlib.Algebra.Module.LocalizedModule.Submodule` `Mathlib.Algebra.Module.Pi` `Mathlib.Algebra.Module.Presentation.Basic` `Mathlib.Algebra.Module.Presentation.Cokernel` `Mathlib.Algebra.Module.Presentation.DirectSum` `Mathlib.Algebra.Module.Presentation.Finite` `Mathlib.Algebra.Module.Presentation.Free` `Mathlib.Algebra.Module.Presentation.RestrictScalars` `Mathlib.Algebra.Module.Presentation.Tautological` `Mathlib.Algebra.Module.Presentation.Tensor` `Mathlib.Algebra.Module.Projective` `Mathlib.Algebra.Module.Rat` `Mathlib.Algebra.Module.SnakeLemma` `Mathlib.Algebra.Module.SpanRank` `Mathlib.Algebra.Module.Submodule.Basic` `Mathlib.Algebra.Module.Submodule.Bilinear` `Mathlib.Algebra.Module.Submodule.Defs` `Mathlib.Algebra.Module.Submodule.EqLocus` `Mathlib.Algebra.Module.Submodule.Equiv` `Mathlib.Algebra.Module.Submodule.Invariant` `Mathlib.Algebra.Module.Submodule.IterateMapComap` `Mathlib.Algebra.Module.Submodule.Ker` `Mathlib.Algebra.Module.Submodule.Lattice` `Mathlib.Algebra.Module.Submodule.LinearMap` `Mathlib.Algebra.Module.Submodule.Map` `Mathlib.Algebra.Module.Submodule.Order` `Mathlib.Algebra.Module.Submodule.Pointwise` `Mathlib.Algebra.Module.Submodule.Range` `Mathlib.Algebra.Module.Submodule.RestrictScalars` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.Algebra.MonoidAlgebra.Defs` `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Algebra.MonoidAlgebra.Division` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.Algebra.MonoidAlgebra.Ideal` `Mathlib.Algebra.MonoidAlgebra.MapDomain` `Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.Algebra.MvPolynomial.Eval` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.Algebra.MvPolynomial.SchwartzZippel` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.Algebra.NoZeroSMulDivisors.Basic` `Mathlib.Algebra.NoZeroSMulDivisors.Defs` `Mathlib.Algebra.NoZeroSMulDivisors.Pi` `Mathlib.Algebra.NoZeroSMulDivisors.Prod` `Mathlib.Algebra.Order.Algebra` `Mathlib.Algebra.Order.Antidiag.Finsupp` `Mathlib.Algebra.Order.Antidiag.Nat` `Mathlib.Algebra.Order.Antidiag.Pi` `Mathlib.Algebra.Order.Antidiag.Prod` `Mathlib.Algebra.Order.BigOperators.Expect` `Mathlib.Algebra.Order.BigOperators.Group.Finset` `Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite` `Mathlib.Algebra.Order.BigOperators.Ring.Finset` `Mathlib.Algebra.Order.CauSeq.Basic` `Mathlib.Algebra.Order.CauSeq.Completion` `Mathlib.Algebra.Order.Chebyshev` `Mathlib.Algebra.Order.Disjointed` `Mathlib.Algebra.Order.Floor.Div` `Mathlib.Algebra.Order.Group.Cyclic` `Mathlib.Algebra.Order.Group.Finset` `Mathlib.Algebra.Order.Group.Indicator` `Mathlib.Algebra.Order.Group.Int.Sum` `Mathlib.Algebra.Order.Group.Pointwise.Interval` `Mathlib.Algebra.Order.Interval.Basic` `Mathlib.Algebra.Order.Interval.Finset.Basic` `Mathlib.Algebra.Order.Interval.Finset.SuccPred` `Mathlib.Algebra.Order.Interval.Multiset` `Mathlib.Algebra.Order.Module.Algebra` `Mathlib.Algebra.Order.Module.Defs` `Mathlib.Algebra.Order.Module.OrderedSMul` `Mathlib.Algebra.Order.Module.Pointwise` `Mathlib.Algebra.Order.Module.Rat` `Mathlib.Algebra.Order.Monovary` `Mathlib.Algebra.Order.Nonneg.Module` `Mathlib.Algebra.Order.PartialSups` `Mathlib.Algebra.Order.Pi` `Mathlib.Algebra.Order.Rearrangement` `Mathlib.Algebra.Order.Ring.IsNonarchimedean` `Mathlib.Algebra.Order.Ring.Star` `Mathlib.Algebra.Order.Star.Basic` `Mathlib.Algebra.Order.Star.Conjneg` `Mathlib.Algebra.Order.Star.Prod` `Mathlib.Algebra.Order.UpperLower` `Mathlib.Algebra.Pointwise.Stabilizer` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Polynomial.Basis` `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Algebra.Polynomial.Cardinal` `Mathlib.Algebra.Polynomial.CoeffList` `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Algebra.Polynomial.Coeff` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Algebra.Polynomial.Degree.Definitions` `Mathlib.Algebra.Polynomial.Degree.Domain` `Mathlib.Algebra.Polynomial.Degree.Lemmas` `Mathlib.Algebra.Polynomial.Degree.Monomial` `Mathlib.Algebra.Polynomial.Degree.Operations` `Mathlib.Algebra.Polynomial.Degree.SmallDegree` `Mathlib.Algebra.Polynomial.Degree.Support` `Mathlib.Algebra.Polynomial.Degree.TrailingDegree` `Mathlib.Algebra.Polynomial.Degree.Units` `Mathlib.Algebra.Polynomial.DenomsClearable` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Algebra.Polynomial.Derivative` `Mathlib.Algebra.Polynomial.Div` `Mathlib.Algebra.Polynomial.EraseLead` `Mathlib.Algebra.Polynomial.Eval.Algebra` `Mathlib.Algebra.Polynomial.Eval.Coeff` `Mathlib.Algebra.Polynomial.Eval.Defs` `Mathlib.Algebra.Polynomial.Eval.Degree` `Mathlib.Algebra.Polynomial.Eval.Irreducible` `Mathlib.Algebra.Polynomial.Eval.SMul` `Mathlib.Algebra.Polynomial.Eval.Subring` `Mathlib.Algebra.Polynomial.Expand` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Algebra.Polynomial.GroupRingAction` `Mathlib.Algebra.Polynomial.HasseDeriv` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.Algebra.Polynomial.OfFn` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Algebra.Polynomial.Reverse` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Algebra.Polynomial.Sequence` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.Algebra.Polynomial.UnitTrinomial` `Mathlib.Algebra.PresentedMonoid.Basic` `Mathlib.Algebra.QuadraticDiscriminant` `Mathlib.Algebra.Quandle` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Quaternion` `Mathlib.Algebra.Regular.Pow` `Mathlib.Algebra.Ring.Action.ConjAct` `Mathlib.Algebra.Ring.Action.End` `Mathlib.Algebra.Ring.Action.Group` `Mathlib.Algebra.Ring.Action.Pointwise.Finset` `Mathlib.Algebra.Ring.Action.Submonoid` `Mathlib.Algebra.Ring.AddAut` `Mathlib.Algebra.Ring.Aut` `Mathlib.Algebra.Ring.CentroidHom` `Mathlib.Algebra.Ring.Divisibility.Lemmas` `Mathlib.Algebra.Ring.NegOnePow` `Mathlib.Algebra.Ring.NonZeroDivisors` `Mathlib.Algebra.Ring.Periodic` `Mathlib.Algebra.Ring.Pi` `Mathlib.Algebra.Ring.Pointwise.Finset` `Mathlib.Algebra.Ring.Semireal.Defs` `Mathlib.Algebra.Ring.Subgroup` `Mathlib.Algebra.Ring.Submonoid.Pointwise` `Mathlib.Algebra.Ring.Subring.Basic` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.Algebra.Ring.Subring.MulOpposite` `Mathlib.Algebra.Ring.Subring.Pointwise` `Mathlib.Algebra.Ring.Subring.Units` `Mathlib.Algebra.Ring.Subsemiring.Basic` `Mathlib.Algebra.Ring.Subsemiring.MulOpposite` `Mathlib.Algebra.Ring.Subsemiring.Pointwise` `Mathlib.Algebra.Ring.SumsOfSquares` `Mathlib.Algebra.RingQuot` `Mathlib.Algebra.SkewMonoidAlgebra.Basic` `Mathlib.Algebra.Small.Group` `Mathlib.Algebra.Small.Module` `Mathlib.Algebra.Small.Ring` `Mathlib.Algebra.Squarefree.Basic` `Mathlib.Algebra.Star.Basic` `Mathlib.Algebra.Star.BigOperators` `Mathlib.Algebra.Star.Center` `Mathlib.Algebra.Star.CentroidHom` `Mathlib.Algebra.Star.Conjneg` `Mathlib.Algebra.Star.Free` `Mathlib.Algebra.Star.Module` `Mathlib.Algebra.Star.NonUnitalSubalgebra` `Mathlib.Algebra.Star.NonUnitalSubsemiring` `Mathlib.Algebra.Star.Pi` `Mathlib.Algebra.Star.Pointwise` `Mathlib.Algebra.Star.Prod` `Mathlib.Algebra.Star.Rat` `Mathlib.Algebra.Star.RingQuot` `Mathlib.Algebra.Star.SelfAdjoint` `Mathlib.Algebra.Star.StarAlgHom` `Mathlib.Algebra.Star.StarRingHom` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.Algebra.Star.Subsemiring` `Mathlib.Algebra.Star.Unitary` `Mathlib.Algebra.Symmetrized` `Mathlib.Algebra.TrivSqZeroExt` `Mathlib.Algebra.Tropical.BigOperators` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Algebra.Vertex.VertexOperator` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.Group` `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.AlgebraicTopology.CechNerve` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.AlgebraicTopology.ModelCategory.Basic` `Mathlib.AlgebraicTopology.MooreComplex` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells` `Mathlib.AlgebraicTopology.RelativeCellComplex.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono` `Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.AlgebraicTopology.SimplicialObject.Basic` `Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialObject.Split` `Mathlib.AlgebraicTopology.SimplicialSet.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.Boundary` `Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations` `Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialSet.Degenerate` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.AlgebraicTopology.SimplicialSet.Horn` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction` `Mathlib.AlgebraicTopology.SimplicialSet.Nerve` `Mathlib.AlgebraicTopology.SimplicialSet.Path` `Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex` `Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal` `Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex` `Mathlib.Analysis.Convex.Basic` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Analysis.Convex.Combination` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.Analysis.Convex.Extreme` `Mathlib.Analysis.Convex.Function` `Mathlib.Analysis.Convex.Hull` `Mathlib.Analysis.Convex.Independent` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Analysis.Convex.Join` `Mathlib.Analysis.Convex.Mul` `Mathlib.Analysis.Convex.Piecewise` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Convex.Radon` `Mathlib.Analysis.Convex.Segment` `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.Analysis.Convex.Slope` `Mathlib.Analysis.Convex.Star` `Mathlib.Analysis.Convex.StoneSeparation` `Mathlib.CategoryTheory.Abelian.Basic` `Mathlib.CategoryTheory.Abelian.CommSq` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp` `Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.CategoryTheory.Abelian.FreydMitchell` `Mathlib.CategoryTheory.Abelian.FunctorCategory` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject` `Mathlib.CategoryTheory.Abelian.Indization` `Mathlib.CategoryTheory.Abelian.Injective.Basic` `Mathlib.CategoryTheory.Abelian.Injective.Resolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.Monomorphisms` `Mathlib.CategoryTheory.Abelian.NonPreadditive` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.CategoryTheory.Abelian.Projective.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Dimension` `Mathlib.CategoryTheory.Abelian.Projective.Resolution` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Abelian.SerreClass.Basic` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.CategoryTheory.Abelian.Transfer` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Action.Basic` `Mathlib.CategoryTheory.Action.Concrete` `Mathlib.CategoryTheory.Action.Continuous` `Mathlib.CategoryTheory.Action.Limits` `Mathlib.CategoryTheory.Action.Monoidal` `Mathlib.CategoryTheory.Action` `Mathlib.CategoryTheory.Adhesive` `Mathlib.CategoryTheory.Adjunction.Additive` `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.Adjunction.Lifting.Left` `Mathlib.CategoryTheory.Adjunction.Lifting.Right` `Mathlib.CategoryTheory.Category.Cat.Colimit` `Mathlib.CategoryTheory.Center.Linear` `Mathlib.CategoryTheory.Center.Localization` `Mathlib.CategoryTheory.ChosenFiniteProducts.Cat` `Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory` `Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice` `Mathlib.CategoryTheory.ChosenFiniteProducts.Over` `Mathlib.CategoryTheory.ChosenFiniteProducts` `Mathlib.CategoryTheory.Closed.Cartesian` `Mathlib.CategoryTheory.Closed.Enrichment` `Mathlib.CategoryTheory.Closed.FunctorCategory.Basic` `Mathlib.CategoryTheory.Closed.FunctorCategory.Complete` `Mathlib.CategoryTheory.Closed.FunctorToTypes` `Mathlib.CategoryTheory.Closed.Functor` `Mathlib.CategoryTheory.Closed.Ideal` `Mathlib.CategoryTheory.Closed.Types` `Mathlib.CategoryTheory.Closed.Zero` `Mathlib.CategoryTheory.CofilteredSystem` `Mathlib.CategoryTheory.Comma.CardinalArrow` `Mathlib.CategoryTheory.Comma.Final` `Mathlib.CategoryTheory.Comma.Presheaf.Colimit` `Mathlib.CategoryTheory.Comma.StructuredArrow.Final` `Mathlib.CategoryTheory.ConcreteCategory.EpiMono` `Mathlib.CategoryTheory.Dialectica.Basic` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.CategoryTheory.Distributive.Cartesian` `Mathlib.CategoryTheory.Distributive.Monoidal` `Mathlib.CategoryTheory.EffectiveEpi.Extensive` `Mathlib.CategoryTheory.Enriched.Basic` `Mathlib.CategoryTheory.Enriched.FunctorCategory` `Mathlib.CategoryTheory.Enriched.HomCongr` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal` `Mathlib.CategoryTheory.Enriched.Opposite` `Mathlib.CategoryTheory.Enriched.Ordinary.Basic` `Mathlib.CategoryTheory.Extensive` `Mathlib.CategoryTheory.Filtered.Basic` `Mathlib.CategoryTheory.Filtered.Connected` `Mathlib.CategoryTheory.Filtered.CostructuredArrow` `Mathlib.CategoryTheory.Filtered.Final` `Mathlib.CategoryTheory.Filtered.Flat` `Mathlib.CategoryTheory.Filtered.Grothendieck` `Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Filtered.Small` `Mathlib.CategoryTheory.FintypeCat` `Mathlib.CategoryTheory.Functor.Flat` `Mathlib.CategoryTheory.Functor.FunctorHom` `Mathlib.CategoryTheory.Galois.Action` `Mathlib.CategoryTheory.Galois.Basic` `Mathlib.CategoryTheory.Galois.Decomposition` `Mathlib.CategoryTheory.Galois.Examples` `Mathlib.CategoryTheory.Galois.Full` `Mathlib.CategoryTheory.Galois.GaloisObjects` `Mathlib.CategoryTheory.Galois.Prorepresentability` `Mathlib.CategoryTheory.Generator.Abelian` `Mathlib.CategoryTheory.Generator.Basic` `Mathlib.CategoryTheory.Generator.HomologicalComplex` `Mathlib.CategoryTheory.Generator.Indization` `Mathlib.CategoryTheory.Generator.Preadditive` `Mathlib.CategoryTheory.Generator.Presheaf` `Mathlib.CategoryTheory.Generator.Sheaf` `Mathlib.CategoryTheory.GlueData` `Mathlib.CategoryTheory.GradedObject.Braiding` `Mathlib.CategoryTheory.GradedObject.Monoidal` `Mathlib.CategoryTheory.GuitartExact.Basic` `Mathlib.CategoryTheory.GuitartExact.Opposite` `Mathlib.CategoryTheory.GuitartExact.VerticalComposition` `Mathlib.CategoryTheory.Idempotents.Basic` `Mathlib.CategoryTheory.Idempotents.Biproducts` `Mathlib.CategoryTheory.Idempotents.FunctorCategories` `Mathlib.CategoryTheory.Idempotents.FunctorExtension` `Mathlib.CategoryTheory.Idempotents.HomologicalComplex` `Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi` `Mathlib.CategoryTheory.Idempotents.Karoubi` `Mathlib.CategoryTheory.Idempotents.SimplicialObject` `Mathlib.CategoryTheory.Join.Final` `Mathlib.CategoryTheory.LiftingProperties.Limits` `Mathlib.CategoryTheory.Limits.Comma` `Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic` `Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures` `Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.EpiMono` `Mathlib.CategoryTheory.Limits.Constructions.Equalizers` `Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant` `Mathlib.CategoryTheory.Limits.Constructions.Filtered` `Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers` `Mathlib.CategoryTheory.Limits.Constructions.Over.Basic` `Mathlib.CategoryTheory.Limits.Constructions.Over.Products` `Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects` `Mathlib.CategoryTheory.Limits.EpiMono` `Mathlib.CategoryTheory.Limits.ExactFunctor` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct` `Mathlib.CategoryTheory.Limits.Filtered` `Mathlib.CategoryTheory.Limits.Final.ParallelPair` `Mathlib.CategoryTheory.Limits.Final` `Mathlib.CategoryTheory.Limits.FinallySmall` `Mathlib.CategoryTheory.Limits.FintypeCat` `Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono` `Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered` `Mathlib.CategoryTheory.Limits.FunctorCategory.Finite` `Mathlib.CategoryTheory.Limits.IndYoneda` `Mathlib.CategoryTheory.Limits.Indization.Category` `Mathlib.CategoryTheory.Limits.Indization.Equalizers` `Mathlib.CategoryTheory.Limits.Indization.FilteredColimits` `Mathlib.CategoryTheory.Limits.Indization.IndObject` `Mathlib.CategoryTheory.Limits.Indization.LocallySmall` `Mathlib.CategoryTheory.Limits.Indization.ParallelPair` `Mathlib.CategoryTheory.Limits.Indization.Products` `Mathlib.CategoryTheory.Limits.IsConnected` `Mathlib.CategoryTheory.Limits.Lattice` `Mathlib.CategoryTheory.Limits.MorphismProperty` `Mathlib.CategoryTheory.Limits.Opposites` `Mathlib.CategoryTheory.Limits.Over` `Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite` `Mathlib.CategoryTheory.Limits.Preserves.Filtered` `Mathlib.CategoryTheory.Limits.Preserves.Finite` `Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory` `Mathlib.CategoryTheory.Limits.Preserves.Opposites` `Mathlib.CategoryTheory.Limits.Preserves.Over` `Mathlib.CategoryTheory.Limits.Preserves.Presheaf` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square` `Mathlib.CategoryTheory.Limits.Presheaf` `Mathlib.CategoryTheory.Limits.Set` `Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts` `Mathlib.CategoryTheory.Limits.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory` `Mathlib.CategoryTheory.Limits.Shapes.Countable` `Mathlib.CategoryTheory.Limits.Shapes.Diagonal` `Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits` `Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer` `Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts` `Mathlib.CategoryTheory.Limits.Shapes.KernelPair` `Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square` `Mathlib.CategoryTheory.Limits.Shapes.Reflexive` `Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct` `Mathlib.CategoryTheory.Limits.Shapes.SingleObj` `Mathlib.CategoryTheory.Limits.Sifted` `Mathlib.CategoryTheory.Limits.SmallComplete` `Mathlib.CategoryTheory.Limits.Types.Filtered` `Mathlib.CategoryTheory.Limits.VanKampen` `Mathlib.CategoryTheory.Linear.Basic` `Mathlib.CategoryTheory.Linear.FunctorCategory` `Mathlib.CategoryTheory.Linear.LinearFunctor` `Mathlib.CategoryTheory.Linear.Yoneda` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.CategoryTheory.Localization.Linear` `Mathlib.CategoryTheory.Localization.Pi` `Mathlib.CategoryTheory.Localization.Preadditive` `Mathlib.CategoryTheory.Localization.SmallShiftedHom` `Mathlib.CategoryTheory.Localization.Triangulated` `Mathlib.CategoryTheory.Monad.Coequalizer` `Mathlib.CategoryTheory.Monad.Comonadicity` `Mathlib.CategoryTheory.Monad.Equalizer` `Mathlib.CategoryTheory.Monad.Monadicity` `Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_` `Mathlib.CategoryTheory.Monoidal.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Grp_` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_` `Mathlib.CategoryTheory.Monoidal.Linear` `Mathlib.CategoryTheory.Monoidal.Preadditive` `Mathlib.CategoryTheory.Monoidal.Subcategory` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.CategoryTheory.Monoidal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Types.Coyoneda` `Mathlib.CategoryTheory.MorphismProperty.Descent` `Mathlib.CategoryTheory.MorphismProperty.FunctorCategory` `Mathlib.CategoryTheory.MorphismProperty.LiftingProperty` `Mathlib.CategoryTheory.MorphismProperty.Limits` `Mathlib.CategoryTheory.MorphismProperty.OverAdjunction` `Mathlib.CategoryTheory.MorphismProperty.Representable` `Mathlib.CategoryTheory.MorphismProperty.RetractArgument` `Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition` `Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem` `Mathlib.CategoryTheory.Noetherian` `Mathlib.CategoryTheory.ObjectProperty.EpiMono` `Mathlib.CategoryTheory.ObjectProperty.Extensions` `Mathlib.CategoryTheory.Preadditive.AdditiveFunctor` `Mathlib.CategoryTheory.Preadditive.Basic` `Mathlib.CategoryTheory.Preadditive.Biproducts` `Mathlib.CategoryTheory.Preadditive.CommGrp_` `Mathlib.CategoryTheory.Preadditive.EilenbergMoore` `Mathlib.CategoryTheory.Preadditive.EndoFunctor` `Mathlib.CategoryTheory.Preadditive.FunctorCategory` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.CategoryTheory.Preadditive.Indization` `Mathlib.CategoryTheory.Preadditive.Injective.Basic` `Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties` `Mathlib.CategoryTheory.Preadditive.Injective.Preserves` `Mathlib.CategoryTheory.Preadditive.Injective.Resolution` `Mathlib.CategoryTheory.Preadditive.LeftExact` `Mathlib.CategoryTheory.Preadditive.LiftToFinset` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.CategoryTheory.Preadditive.OfBiproducts` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.CategoryTheory.Preadditive.Projective.Basic` `Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties` `Mathlib.CategoryTheory.Preadditive.Projective.Preserves` `Mathlib.CategoryTheory.Preadditive.Projective.Resolution` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.CategoryTheory.Preadditive.SingleObj` `Mathlib.CategoryTheory.Preadditive.Transfer` `Mathlib.CategoryTheory.Preadditive.Yoneda.Basic` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.CategoryTheory.Presentable.Basic` `Mathlib.CategoryTheory.Presentable.Finite` `Mathlib.CategoryTheory.Presentable.IsCardinalFiltered` `Mathlib.CategoryTheory.Presentable.Limits` `Mathlib.CategoryTheory.Quotient.Linear` `Mathlib.CategoryTheory.Quotient.Preadditive` `Mathlib.CategoryTheory.Shift.InducedShiftSequence` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.CategoryTheory.Shift.Pullback` `Mathlib.CategoryTheory.Shift.ShiftSequence` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.CategoryTheory.Shift.ShiftedHom` `Mathlib.CategoryTheory.Simple` `Mathlib.CategoryTheory.Sites.Abelian` `Mathlib.CategoryTheory.Sites.Adjunction` `Mathlib.CategoryTheory.Sites.Canonical` `Mathlib.CategoryTheory.Sites.CartesianClosed` `Mathlib.CategoryTheory.Sites.ChosenFiniteProducts` `Mathlib.CategoryTheory.Sites.Coherent.Basic` `Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves` `Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology` `Mathlib.CategoryTheory.Sites.Coherent.Comparison` `Mathlib.CategoryTheory.Sites.Coherent.Equivalence` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology` `Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular` `Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves` `Mathlib.CategoryTheory.Sites.Coherent.RegularTopology` `Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit` `Mathlib.CategoryTheory.Sites.Coherent.SheafComparison` `Mathlib.CategoryTheory.Sites.CompatiblePlus` `Mathlib.CategoryTheory.Sites.CompatibleSheafification` `Mathlib.CategoryTheory.Sites.ConcreteSheafification` `Mathlib.CategoryTheory.Sites.ConstantSheaf` `Mathlib.CategoryTheory.Sites.Continuous` `Mathlib.CategoryTheory.Sites.CoverLifting` `Mathlib.CategoryTheory.Sites.CoverPreserving` `Mathlib.CategoryTheory.Sites.Coverage` `Mathlib.CategoryTheory.Sites.CoversTop` `Mathlib.CategoryTheory.Sites.DenseSubsite.Basic` `Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology` `Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv` `Mathlib.CategoryTheory.Sites.EpiMono` `Mathlib.CategoryTheory.Sites.Equivalence` `Mathlib.CategoryTheory.Sites.GlobalSections` `Mathlib.CategoryTheory.Sites.IsSheafOneHypercover` `Mathlib.CategoryTheory.Sites.LeftExact` `Mathlib.CategoryTheory.Sites.Limits` `Mathlib.CategoryTheory.Sites.Localization` `Mathlib.CategoryTheory.Sites.LocallyBijective` `Mathlib.CategoryTheory.Sites.LocallyFullyFaithful` `Mathlib.CategoryTheory.Sites.LocallyInjective` `Mathlib.CategoryTheory.Sites.LocallySurjective` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.CategoryTheory.Sites.Monoidal` `Mathlib.CategoryTheory.Sites.MorphismProperty` `Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1` `Mathlib.CategoryTheory.Sites.OneHypercover` `Mathlib.CategoryTheory.Sites.Over` `Mathlib.CategoryTheory.Sites.Plus` `Mathlib.CategoryTheory.Sites.PreservesLocallyBijective` `Mathlib.CategoryTheory.Sites.PreservesSheafification` `Mathlib.CategoryTheory.Sites.Preserves` `Mathlib.CategoryTheory.Sites.Pullback` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.CategoryTheory.Sites.SheafHom` `Mathlib.CategoryTheory.Sites.Sheaf` `Mathlib.CategoryTheory.Sites.Sheafification` `Mathlib.CategoryTheory.Sites.Spaces` `Mathlib.CategoryTheory.Sites.Subcanonical` `Mathlib.CategoryTheory.Sites.Subsheaf` `Mathlib.CategoryTheory.Sites.Types` `Mathlib.CategoryTheory.Sites.Whiskering` `Mathlib.CategoryTheory.SmallObject.Basic` `Mathlib.CategoryTheory.SmallObject.Construction` `Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument` `Mathlib.CategoryTheory.SmallObject.Iteration.Basic` `Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc` `Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone` `Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty` `Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting` `Mathlib.CategoryTheory.SmallObject.TransfiniteIteration` `Mathlib.CategoryTheory.Subobject.Basic` `Mathlib.CategoryTheory.Subobject.Comma` `Mathlib.CategoryTheory.Subobject.FactorThru` `Mathlib.CategoryTheory.Subobject.HasCardinalLT` `Mathlib.CategoryTheory.Subobject.Lattice` `Mathlib.CategoryTheory.Subobject.Limits` `Mathlib.CategoryTheory.Subobject.MonoOver` `Mathlib.CategoryTheory.Subobject.NoetherianObject` `Mathlib.CategoryTheory.Subobject.Presheaf` `Mathlib.CategoryTheory.Subobject.Types` `Mathlib.CategoryTheory.Subobject.WellPowered` `Mathlib.CategoryTheory.Subpresheaf.Equalizer` `Mathlib.CategoryTheory.Subpresheaf.Finite` `Mathlib.CategoryTheory.Subpresheaf.Image` `Mathlib.CategoryTheory.Subpresheaf.OfSection` `Mathlib.CategoryTheory.Subpresheaf.Subobject` `Mathlib.CategoryTheory.Subterminal` `Mathlib.CategoryTheory.Topos.Classifier` `Mathlib.CategoryTheory.Triangulated.Adjunction` `Mathlib.CategoryTheory.Triangulated.Basic` `Mathlib.CategoryTheory.Triangulated.Functor` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.CategoryTheory.Triangulated.Opposite.Basic` `Mathlib.CategoryTheory.Triangulated.Opposite.Functor` `Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangle` `Mathlib.CategoryTheory.Triangulated.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Rotate` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.CategoryTheory.Triangulated.TStructure.Basic` `Mathlib.CategoryTheory.Triangulated.TriangleShift` `Mathlib.CategoryTheory.Triangulated.Triangulated` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.CategoryTheory.WithTerminal.FinCategory` `Mathlib.Combinatorics.Additive.AP.Three.Defs` `Mathlib.Combinatorics.Additive.ApproximateSubgroup` `Mathlib.Combinatorics.Additive.CauchyDavenport` `Mathlib.Combinatorics.Additive.Corner.Defs` `Mathlib.Combinatorics.Additive.CovBySMul` `Mathlib.Combinatorics.Additive.Dissociation` `Mathlib.Combinatorics.Additive.DoublingConst` `Mathlib.Combinatorics.Additive.ETransform` `Mathlib.Combinatorics.Additive.Energy` `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` `Mathlib.Combinatorics.Additive.FreimanHom` `Mathlib.Combinatorics.Additive.PluenneckeRuzsa` `Mathlib.Combinatorics.Additive.RuzsaCovering` `Mathlib.Combinatorics.Additive.SmallTripling` `Mathlib.Combinatorics.Additive.VerySmallDoubling` `Mathlib.Combinatorics.Colex` `Mathlib.Combinatorics.Configuration` `Mathlib.Combinatorics.Derangements.Basic` `Mathlib.Combinatorics.Derangements.Finite` `Mathlib.Combinatorics.Digraph.Basic` `Mathlib.Combinatorics.Digraph.Orientation` `Mathlib.Combinatorics.Enumerative.Bell` `Mathlib.Combinatorics.Enumerative.Catalan` `Mathlib.Combinatorics.Enumerative.Composition` `Mathlib.Combinatorics.Enumerative.DoubleCounting` `Mathlib.Combinatorics.Enumerative.DyckWord` `Mathlib.Combinatorics.Enumerative.IncidenceAlgebra` `Mathlib.Combinatorics.Enumerative.InclusionExclusion` `Mathlib.Combinatorics.Enumerative.Partition` `Mathlib.Combinatorics.HalesJewett` `Mathlib.Combinatorics.Hall.Basic` `Mathlib.Combinatorics.Hall.Finite` `Mathlib.Combinatorics.Hindman` `Mathlib.Combinatorics.Nullstellensatz` `Mathlib.Combinatorics.Optimization.ValuedCSP` `Mathlib.Combinatorics.Pigeonhole` `Mathlib.Combinatorics.SetFamily.AhlswedeZhang` `Mathlib.Combinatorics.SetFamily.Compression.UV` `Mathlib.Combinatorics.SetFamily.FourFunctions` `Mathlib.Combinatorics.SetFamily.HarrisKleitman` `Mathlib.Combinatorics.SetFamily.Kleitman` `Mathlib.Combinatorics.SetFamily.KruskalKatona` `Mathlib.Combinatorics.SetFamily.LYM` `Mathlib.Combinatorics.SetFamily.Shadow` `Mathlib.Combinatorics.SetFamily.Shatter` `Mathlib.Combinatorics.SimpleGraph.Acyclic` `Mathlib.Combinatorics.SimpleGraph.AdjMatrix` `Mathlib.Combinatorics.SimpleGraph.Basic` `Mathlib.Combinatorics.SimpleGraph.Bipartite` `Mathlib.Combinatorics.SimpleGraph.Circulant` `Mathlib.Combinatorics.SimpleGraph.Clique` `Mathlib.Combinatorics.SimpleGraph.Coloring` `Mathlib.Combinatorics.SimpleGraph.ConcreteColorings` `Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents` `Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph` `Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting` `Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp` `Mathlib.Combinatorics.SimpleGraph.Copy` `Mathlib.Combinatorics.SimpleGraph.Dart` `Mathlib.Combinatorics.SimpleGraph.DegreeSum` `Mathlib.Combinatorics.SimpleGraph.DeleteEdges` `Mathlib.Combinatorics.SimpleGraph.Density` `Mathlib.Combinatorics.SimpleGraph.Diam` `Mathlib.Combinatorics.SimpleGraph.Ends.Defs` `Mathlib.Combinatorics.SimpleGraph.Ends.Properties` `Mathlib.Combinatorics.SimpleGraph.Extremal.Basic` `Mathlib.Combinatorics.SimpleGraph.Finite` `Mathlib.Combinatorics.SimpleGraph.Finsubgraph` `Mathlib.Combinatorics.SimpleGraph.Girth` `Mathlib.Combinatorics.SimpleGraph.Hamiltonian` `Mathlib.Combinatorics.SimpleGraph.Hasse` `Mathlib.Combinatorics.SimpleGraph.IncMatrix` `Mathlib.Combinatorics.SimpleGraph.LineGraph` `Mathlib.Combinatorics.SimpleGraph.Maps` `Mathlib.Combinatorics.SimpleGraph.Matching` `Mathlib.Combinatorics.SimpleGraph.Metric` `Mathlib.Combinatorics.SimpleGraph.Operations` `Mathlib.Combinatorics.SimpleGraph.Partition` `Mathlib.Combinatorics.SimpleGraph.Path` `Mathlib.Combinatorics.SimpleGraph.Prod` `Mathlib.Combinatorics.SimpleGraph.Regularity.Energy` `Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise` `Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform` `Mathlib.Combinatorics.SimpleGraph.StronglyRegular` `Mathlib.Combinatorics.SimpleGraph.Subgraph` `Mathlib.Combinatorics.SimpleGraph.Sum` `Mathlib.Combinatorics.SimpleGraph.Trails` `Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SimpleGraph.Triangle.Counting` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite` `Mathlib.Combinatorics.SimpleGraph.Turan` `Mathlib.Combinatorics.SimpleGraph.Tutte` `Mathlib.Combinatorics.SimpleGraph.UniversalVerts` `Mathlib.Combinatorics.SimpleGraph.Walk` `Mathlib.Combinatorics.Young.SemistandardTableau` `Mathlib.Combinatorics.Young.YoungDiagram` `Mathlib.Computability.ContextFreeGrammar` `Mathlib.Computability.DFA` `Mathlib.Computability.Encoding` `Mathlib.Computability.EpsilonNFA` `Mathlib.Computability.Language` `Mathlib.Computability.MyhillNerode` `Mathlib.Computability.NFA` `Mathlib.Computability.PostTuringMachine` `Mathlib.Computability.RegularExpressions` `Mathlib.Computability.TMComputable` `Mathlib.Computability.TMConfig` `Mathlib.Computability.TMToPartrec` `Mathlib.Computability.TuringMachine` `Mathlib.Control.LawfulFix` `Mathlib.Data.Analysis.Filter` `Mathlib.Data.Analysis.Topology` `Mathlib.Data.Complex.Basic` `Mathlib.Data.Complex.BigOperators` `Mathlib.Data.Complex.Determinant` `Mathlib.Data.Complex.Module` `Mathlib.Data.Complex.Orientation` `Mathlib.Data.DFinsupp.BigOperators` `Mathlib.Data.DFinsupp.FiniteInfinite` `Mathlib.Data.DFinsupp.Interval` `Mathlib.Data.DFinsupp.Lex` `Mathlib.Data.DFinsupp.Module` `Mathlib.Data.DFinsupp.Multiset` `Mathlib.Data.DFinsupp.Notation` `Mathlib.Data.DFinsupp.Order` `Mathlib.Data.DFinsupp.Sigma` `Mathlib.Data.DFinsupp.Small` `Mathlib.Data.DFinsupp.Submonoid` `Mathlib.Data.DFinsupp.WellFounded` `Mathlib.Data.ENat.BigOperators` `Mathlib.Data.ENat.Lattice` `Mathlib.Data.Fin.Tuple.BubbleSortInduction` `Mathlib.Data.Fin.Tuple.Finset` `Mathlib.Data.Fin.Tuple.NatAntidiagonal` `Mathlib.Data.Fin.Tuple.Reflection` `Mathlib.Data.Fin.Tuple.Sort` `Mathlib.Data.FinEnum.Option` `Mathlib.Data.FinEnum` `Mathlib.Data.Finite.Card` `Mathlib.Data.Finite.Perm` `Mathlib.Data.Finite.Prod` `Mathlib.Data.Finite.Sigma` `Mathlib.Data.Finite.Vector` `Mathlib.Data.Finmap` `Mathlib.Data.Finset.Finsupp` `Mathlib.Data.Finset.Functor` `Mathlib.Data.Finset.Interval` `Mathlib.Data.Finset.Lattice.Pi` `Mathlib.Data.Finset.Lattice.Prod` `Mathlib.Data.Finset.Lattice.Union` `Mathlib.Data.Finset.MulAntidiagonal` `Mathlib.Data.Finset.NAry` `Mathlib.Data.Finset.NatAntidiagonal` `Mathlib.Data.Finset.NatDivisors` `Mathlib.Data.Finset.NoncommProd` `Mathlib.Data.Finset.Option` `Mathlib.Data.Finset.PImage` `Mathlib.Data.Finset.PiInduction` `Mathlib.Data.Finset.Pi` `Mathlib.Data.Finset.Powerset` `Mathlib.Data.Finset.Preimage` `Mathlib.Data.Finset.Prod` `Mathlib.Data.Finset.SMulAntidiagonal` `Mathlib.Data.Finset.Sigma` `Mathlib.Data.Finset.Slice` `Mathlib.Data.Finset.Sups` `Mathlib.Data.Finset.Sym` `Mathlib.Data.Finset.Union` `Mathlib.Data.Finset.Update` `Mathlib.Data.Finsupp.AList` `Mathlib.Data.Finsupp.Antidiagonal` `Mathlib.Data.Finsupp.Basic` `Mathlib.Data.Finsupp.BigOperators` `Mathlib.Data.Finsupp.Encodable` `Mathlib.Data.Finsupp.Ext` `Mathlib.Data.Finsupp.Fin` `Mathlib.Data.Finsupp.Fintype` `Mathlib.Data.Finsupp.Indicator` `Mathlib.Data.Finsupp.Interval` `Mathlib.Data.Finsupp.Lex` `Mathlib.Data.Finsupp.MonomialOrder.DegLex` `Mathlib.Data.Finsupp.MonomialOrder` `Mathlib.Data.Finsupp.Multiset` `Mathlib.Data.Finsupp.Notation` `Mathlib.Data.Finsupp.Order` `Mathlib.Data.Finsupp.PWO` `Mathlib.Data.Finsupp.Pointwise` `Mathlib.Data.Finsupp.SMulWithZero` `Mathlib.Data.Finsupp.SMul` `Mathlib.Data.Finsupp.Single` `Mathlib.Data.Finsupp.ToDFinsupp` `Mathlib.Data.Finsupp.Weight` `Mathlib.Data.Finsupp.WellFounded` `Mathlib.Data.Fintype.BigOperators` `Mathlib.Data.Fintype.CardEmbedding` `Mathlib.Data.Fintype.Fin` `Mathlib.Data.Fintype.List` `Mathlib.Data.Fintype.Option` `Mathlib.Data.Fintype.Perm` `Mathlib.Data.Fintype.Pi` `Mathlib.Data.Fintype.Pigeonhole` `Mathlib.Data.Fintype.Powerset` `Mathlib.Data.Fintype.Prod` `Mathlib.Data.Fintype.Quotient` `Mathlib.Data.Fintype.Sigma` `Mathlib.Data.Fintype.Units` `Mathlib.Data.Fintype.Vector` `Mathlib.Data.FunLike.Fintype` `Mathlib.Data.Holor` `Mathlib.Data.Int.AbsoluteValue` `Mathlib.Data.Int.Interval` `Mathlib.Data.Int.Star` `Mathlib.Data.List.Cycle` `Mathlib.Data.List.Pi` `Mathlib.Data.List.Sym` `Mathlib.Data.List.ToFinsupp` `Mathlib.Data.LocallyFinsupp` `Mathlib.Data.Matrix.Auto` `Mathlib.Data.Matrix.Basic` `Mathlib.Data.Matrix.Basis` `Mathlib.Data.Matrix.Bilinear` `Mathlib.Data.Matrix.Block` `Mathlib.Data.Matrix.CharP` `Mathlib.Data.Matrix.ColumnRowPartitioned` `Mathlib.Data.Matrix.Composition` `Mathlib.Data.Matrix.ConjTranspose` `Mathlib.Data.Matrix.Defs` `Mathlib.Data.Matrix.Diagonal` `Mathlib.Data.Matrix.DoublyStochastic` `Mathlib.Data.Matrix.DualNumber` `Mathlib.Data.Matrix.Hadamard` `Mathlib.Data.Matrix.Invertible` `Mathlib.Data.Matrix.Kronecker` `Mathlib.Data.Matrix.Mul` `Mathlib.Data.Matrix.Notation` `Mathlib.Data.Matrix.PEquiv` `Mathlib.Data.Matrix.Rank` `Mathlib.Data.Matrix.Reflection` `Mathlib.Data.Matrix.RowCol` `Mathlib.Data.Matroid.Basic` `Mathlib.Data.Matroid.Circuit` `Mathlib.Data.Matroid.Closure` `Mathlib.Data.Matroid.Constructions` `Mathlib.Data.Matroid.Dual` `Mathlib.Data.Matroid.IndepAxioms` `Mathlib.Data.Matroid.Loop` `Mathlib.Data.Matroid.Map` `Mathlib.Data.Matroid.Minor.Contract` `Mathlib.Data.Matroid.Minor.Delete` `Mathlib.Data.Matroid.Minor.Order` `Mathlib.Data.Matroid.Minor.Restrict` `Mathlib.Data.Matroid.Rank.Cardinal` `Mathlib.Data.Matroid.Rank.ENat` `Mathlib.Data.Matroid.Rank.Finite` `Mathlib.Data.Matroid.Sum` `Mathlib.Data.Multiset.Antidiagonal` `Mathlib.Data.Multiset.Bind` `Mathlib.Data.Multiset.Fintype` `Mathlib.Data.Multiset.Functor` `Mathlib.Data.Multiset.Interval` `Mathlib.Data.Multiset.Pi` `Mathlib.Data.Multiset.Powerset` `Mathlib.Data.Multiset.Sections` `Mathlib.Data.Multiset.Sym` `Mathlib.Data.NNRat.BigOperators` `Mathlib.Data.NNRat.Lemmas` `Mathlib.Data.Nat.ChineseRemainder` `Mathlib.Data.Nat.Choose.Cast` `Mathlib.Data.Nat.Choose.Factorization` `Mathlib.Data.Nat.Choose.Lucas` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.Data.Nat.Choose.Sum` `Mathlib.Data.Nat.Choose.Vandermonde` `Mathlib.Data.Nat.Digits` `Mathlib.Data.Nat.Factorial.BigOperators` `Mathlib.Data.Nat.Factorial.Cast` `Mathlib.Data.Nat.Factorial.DoubleFactorial` `Mathlib.Data.Nat.Factorial.SuperFactorial` `Mathlib.Data.Nat.Factorization.Basic` `Mathlib.Data.Nat.Factorization.Defs` `Mathlib.Data.Nat.Factorization.Induction` `Mathlib.Data.Nat.Factorization.PrimePow` `Mathlib.Data.Nat.Factorization.Root` `Mathlib.Data.Nat.Fib.Basic` `Mathlib.Data.Nat.Fib.Zeckendorf` `Mathlib.Data.Nat.GCD.BigOperators` `Mathlib.Data.Nat.Lattice` `Mathlib.Data.Nat.Multiplicity` `Mathlib.Data.Nat.Nth` `Mathlib.Data.Nat.PartENat` `Mathlib.Data.Nat.Periodic` `Mathlib.Data.Nat.Prime.Nth` `Mathlib.Data.Nat.PrimeFin` `Mathlib.Data.Nat.Squarefree` `Mathlib.Data.Nat.Totient` `Mathlib.Data.PNat.Factors` `Mathlib.Data.PNat.Interval` `Mathlib.Data.Pi.Interval` `Mathlib.Data.Rat.BigOperators` `Mathlib.Data.Rat.Cardinal` `Mathlib.Data.Rat.Star` `Mathlib.Data.Real.Basic` `Mathlib.Data.Real.Sign` `Mathlib.Data.Real.Star` `Mathlib.Data.Set.Card.Arithmetic` `Mathlib.Data.Set.Card` `Mathlib.Data.Set.Equitable` `Mathlib.Data.Set.Finite.Lattice` `Mathlib.Data.Set.Finite.Lemmas` `Mathlib.Data.Set.Finite.List` `Mathlib.Data.Set.Finite.Monad` `Mathlib.Data.Set.Finite.Powerset` `Mathlib.Data.Set.MemPartition` `Mathlib.Data.Set.MulAntidiagonal` `Mathlib.Data.Set.Pointwise.Support` `Mathlib.Data.Set.SMulAntidiagonal` `Mathlib.Data.Set.Semiring` `Mathlib.Data.Set.Sups` `Mathlib.Data.SetLike.Fintype` `Mathlib.Data.Setoid.Partition.Card` `Mathlib.Data.Setoid.Partition` `Mathlib.Data.Sigma.Interval` `Mathlib.Data.Sign` `Mathlib.Data.Sum.Interval` `Mathlib.Data.Sym.Card` `Mathlib.Data.Sym.Sym2.Finsupp` `Mathlib.Data.Sym.Sym2.Order` `Mathlib.Data.Sym.Sym2` `Mathlib.Data.W.Cardinal` `Mathlib.Data.ZMod.Aut` `Mathlib.Data.ZMod.Basic` `Mathlib.Data.ZMod.Coprime` `Mathlib.Data.ZMod.Factorial` `Mathlib.Data.ZMod.IntUnitsPower` `Mathlib.Data.ZMod.QuotientGroup` `Mathlib.Data.ZMod.QuotientRing` `Mathlib.Data.ZMod.Units` `Mathlib.Data.ZMod.ValMinAbs` `Mathlib.Deprecated.Cardinal.Continuum` `Mathlib.Deprecated.Cardinal.Finite` `Mathlib.Deprecated.Cardinal.PartENat` `Mathlib.Dynamics.BirkhoffSum.Average` `Mathlib.Dynamics.BirkhoffSum.Basic` `Mathlib.Dynamics.FixedPoints.Basic` `Mathlib.Dynamics.FixedPoints.Prufer` `Mathlib.Dynamics.FixedPoints.Topology` `Mathlib.Dynamics.Flow` `Mathlib.Dynamics.Minimal` `Mathlib.Dynamics.Newton` `Mathlib.Dynamics.OmegaLimit` `Mathlib.Dynamics.PeriodicPts.Defs` `Mathlib.Dynamics.PeriodicPts.Lemmas` `Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.ChevalleyWarning` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Extension` `Mathlib.FieldTheory.Finite.Basic` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Finiteness` `Mathlib.FieldTheory.Fixed` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra` `Mathlib.FieldTheory.IntermediateField.Adjoin.Basic` `Mathlib.FieldTheory.IntermediateField.Adjoin.Defs` `Mathlib.FieldTheory.IntermediateField.Algebraic` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure` `Mathlib.FieldTheory.IsAlgClosed.Basic` `Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.FieldTheory.Isaacs` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.KummerPolynomial` `Mathlib.FieldTheory.Minpoly.Basic` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.FieldTheory.Minpoly.IsConjRoot` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.MvRatFunc.Rank` `Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure` `Mathlib.FieldTheory.Normal.Defs` `Mathlib.FieldTheory.NormalizedTrace` `Mathlib.FieldTheory.PerfectClosure` `Mathlib.FieldTheory.Perfect` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.Exponent` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.FieldTheory.Relrank` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.FieldTheory.Separable` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.FieldTheory.SplittingField.IsSplittingField` `Mathlib.FieldTheory.Tower` `Mathlib.Geometry.Group.Growth.LinearLowerBound` `Mathlib.Geometry.Group.Growth.QuotientInter` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.PresheafedSpace` `Mathlib.Geometry.RingedSpace.SheafedSpace` `Mathlib.Geometry.RingedSpace.Stalks` `Mathlib.GroupTheory.Abelianization` `Mathlib.GroupTheory.ClassEquation` `Mathlib.GroupTheory.Commensurable` `Mathlib.GroupTheory.Commutator.Basic` `Mathlib.GroupTheory.Commutator.Finite` `Mathlib.GroupTheory.CommutingProbability` `Mathlib.GroupTheory.Complement` `Mathlib.GroupTheory.Congruence.BigOperators` `Mathlib.GroupTheory.Coprod.Basic` `Mathlib.GroupTheory.CoprodI` `Mathlib.GroupTheory.Coset.Basic` `Mathlib.GroupTheory.Coset.Card` `Mathlib.GroupTheory.Coset.Defs` `Mathlib.GroupTheory.CosetCover` `Mathlib.GroupTheory.Coxeter.Basic` `Mathlib.GroupTheory.Coxeter.Inversion` `Mathlib.GroupTheory.Coxeter.Length` `Mathlib.GroupTheory.Coxeter.Matrix` `Mathlib.GroupTheory.Divisible` `Mathlib.GroupTheory.DoubleCoset` `Mathlib.GroupTheory.Exponent` `Mathlib.GroupTheory.Finiteness` `Mathlib.GroupTheory.FixedPointFree` `Mathlib.GroupTheory.FreeAbelianGroup` `Mathlib.GroupTheory.FreeGroup.Basic` `Mathlib.GroupTheory.FreeGroup.GeneratorEquiv` `Mathlib.GroupTheory.FreeGroup.IsFreeGroup` `Mathlib.GroupTheory.FreeGroup.NielsenSchreier` `Mathlib.GroupTheory.FreeGroup.Reduce` `Mathlib.GroupTheory.Goursat` `Mathlib.GroupTheory.GroupAction.Basic` `Mathlib.GroupTheory.GroupAction.Blocks` `Mathlib.GroupTheory.GroupAction.CardCommute` `Mathlib.GroupTheory.GroupAction.ConjAct` `Mathlib.GroupTheory.GroupAction.Defs` `Mathlib.GroupTheory.GroupAction.DomAct.ActionHom` `Mathlib.GroupTheory.GroupAction.DomAct.Basic` `Mathlib.GroupTheory.GroupAction.FixedPoints` `Mathlib.GroupTheory.GroupAction.FixingSubgroup` `Mathlib.GroupTheory.GroupAction.Iwasawa` `Mathlib.GroupTheory.GroupAction.Period` `Mathlib.GroupTheory.GroupAction.Primitive` `Mathlib.GroupTheory.GroupAction.Quotient` `Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise` `Mathlib.GroupTheory.GroupAction.SubMulAction` `Mathlib.GroupTheory.GroupAction.Transitive` `Mathlib.GroupTheory.GroupExtension.Basic` `Mathlib.GroupTheory.GroupExtension.Defs` `Mathlib.GroupTheory.HNNExtension` `Mathlib.GroupTheory.IndexNormal` `Mathlib.GroupTheory.Index` `Mathlib.GroupTheory.MonoidLocalization.Away` `Mathlib.GroupTheory.MonoidLocalization.Basic` `Mathlib.GroupTheory.MonoidLocalization.Cardinality` `Mathlib.GroupTheory.MonoidLocalization.DivPairs` `Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup` `Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero` `Mathlib.GroupTheory.MonoidLocalization.Order` `Mathlib.GroupTheory.NoncommCoprod` `Mathlib.GroupTheory.NoncommPiCoprod` `Mathlib.GroupTheory.Order.Min` `Mathlib.GroupTheory.OrderOfElement` `Mathlib.GroupTheory.OreLocalization.Cardinality` `Mathlib.GroupTheory.PGroup` `Mathlib.GroupTheory.Perm.Basic` `Mathlib.GroupTheory.Perm.Centralizer` `Mathlib.GroupTheory.Perm.ClosureSwap` `Mathlib.GroupTheory.Perm.Closure` `Mathlib.GroupTheory.Perm.ConjAct` `Mathlib.GroupTheory.Perm.Cycle.Basic` `Mathlib.GroupTheory.Perm.Cycle.Concrete` `Mathlib.GroupTheory.Perm.Cycle.Factors` `Mathlib.GroupTheory.Perm.Cycle.PossibleTypes` `Mathlib.GroupTheory.Perm.Cycle.Type` `Mathlib.GroupTheory.Perm.DomMulAct` `Mathlib.GroupTheory.Perm.Fin` `Mathlib.GroupTheory.Perm.Finite` `Mathlib.GroupTheory.Perm.List` `Mathlib.GroupTheory.Perm.Option` `Mathlib.GroupTheory.Perm.Sign` `Mathlib.GroupTheory.Perm.Subgroup` `Mathlib.GroupTheory.Perm.Support` `Mathlib.GroupTheory.Perm.ViaEmbedding` `Mathlib.GroupTheory.PresentedGroup` `Mathlib.GroupTheory.PushoutI` `Mathlib.GroupTheory.QuotientGroup.Basic` `Mathlib.GroupTheory.QuotientGroup.Defs` `Mathlib.GroupTheory.QuotientGroup.Finite` `Mathlib.GroupTheory.Rank` `Mathlib.GroupTheory.SemidirectProduct` `Mathlib.GroupTheory.Solvable` `Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer` `Mathlib.GroupTheory.SpecificGroups.Alternating` `Mathlib.GroupTheory.SpecificGroups.Cyclic` `Mathlib.GroupTheory.SpecificGroups.Dihedral` `Mathlib.GroupTheory.SpecificGroups.KleinFour` `Mathlib.GroupTheory.SpecificGroups.Quaternion` `Mathlib.GroupTheory.Subgroup.Center` `Mathlib.GroupTheory.Subgroup.Centralizer` `Mathlib.GroupTheory.Subgroup.Saturated` `Mathlib.GroupTheory.Subgroup.Simple` `Mathlib.GroupTheory.Submonoid.Inverses` `Mathlib.GroupTheory.Torsion` `Mathlib.LinearAlgebra.AffineSpace.AffineEquiv` `Mathlib.LinearAlgebra.AffineSpace.AffineMap` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.LinearAlgebra.AffineSpace.Combination` `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional` `Mathlib.LinearAlgebra.AffineSpace.Independent` `Mathlib.LinearAlgebra.AffineSpace.Matrix` `Mathlib.LinearAlgebra.AffineSpace.MidpointZero` `Mathlib.LinearAlgebra.AffineSpace.Midpoint` `Mathlib.LinearAlgebra.AffineSpace.Ordered` `Mathlib.LinearAlgebra.AffineSpace.Pointwise` `Mathlib.LinearAlgebra.AffineSpace.Restrict` `Mathlib.LinearAlgebra.AffineSpace.Slope` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.LinearAlgebra.Alternating.Curry` `Mathlib.LinearAlgebra.Alternating.DomCoprod` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.LinearAlgebra.Basis.Bilinear` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.LinearAlgebra.Basis.Defs` `Mathlib.LinearAlgebra.Basis.Exact` `Mathlib.LinearAlgebra.Basis.Fin` `Mathlib.LinearAlgebra.Basis.Flag` `Mathlib.LinearAlgebra.Basis.Prod` `Mathlib.LinearAlgebra.Basis.SMul` `Mathlib.LinearAlgebra.Basis.Submodule` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.LinearAlgebra.BilinearForm.Basic` `Mathlib.LinearAlgebra.BilinearForm.DualLattice` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.LinearAlgebra.BilinearForm.Orthogonal` `Mathlib.LinearAlgebra.BilinearForm.Properties` `Mathlib.LinearAlgebra.BilinearForm.TensorProduct` `Mathlib.LinearAlgebra.BilinearMap` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange` `Mathlib.LinearAlgebra.CliffordAlgebra.Basic` `Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory` `Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation` `Mathlib.LinearAlgebra.CliffordAlgebra.Contraction` `Mathlib.LinearAlgebra.CliffordAlgebra.Equivs` `Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv` `Mathlib.LinearAlgebra.CliffordAlgebra.Even` `Mathlib.LinearAlgebra.CliffordAlgebra.Fold` `Mathlib.LinearAlgebra.CliffordAlgebra.Grading` `Mathlib.LinearAlgebra.CliffordAlgebra.Inversion` `Mathlib.LinearAlgebra.CliffordAlgebra.Prod` `Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup` `Mathlib.LinearAlgebra.CliffordAlgebra.Star` `Mathlib.LinearAlgebra.Coevaluation` `Mathlib.LinearAlgebra.Contraction` `Mathlib.LinearAlgebra.Countable` `Mathlib.LinearAlgebra.CrossProduct` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.LinearAlgebra.Determinant` `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `Mathlib.LinearAlgebra.Dimension.ErdosKaplansky` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.LinearAlgebra.Dimension.Finrank` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.LinearAlgebra.Dimension.Localization` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Subsingleton` `Mathlib.LinearAlgebra.DirectSum.Basis` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.LinearAlgebra.Dual.Basis` `Mathlib.LinearAlgebra.Dual.Defs` `Mathlib.LinearAlgebra.Dual.Lemmas` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.ExteriorAlgebra.Basic` `Mathlib.LinearAlgebra.ExteriorAlgebra.Grading` `Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating` `Mathlib.LinearAlgebra.ExteriorPower.Basic` `Mathlib.LinearAlgebra.ExteriorPower.Pairing` `Mathlib.LinearAlgebra.FiniteDimensional.Basic` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FiniteDimensional.Lemmas` `Mathlib.LinearAlgebra.FiniteSpan` `Mathlib.LinearAlgebra.Finsupp.Defs` `Mathlib.LinearAlgebra.Finsupp.LSum` `Mathlib.LinearAlgebra.Finsupp.LinearCombination` `Mathlib.LinearAlgebra.Finsupp.Pi` `Mathlib.LinearAlgebra.Finsupp.Span` `Mathlib.LinearAlgebra.Finsupp.SumProd` `Mathlib.LinearAlgebra.Finsupp.Supported` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.LinearAlgebra.FreeAlgebra` `Mathlib.LinearAlgebra.FreeModule.Basic` `Mathlib.LinearAlgebra.FreeModule.Determinant` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient` `Mathlib.LinearAlgebra.FreeModule.Finite.Matrix` `Mathlib.LinearAlgebra.FreeModule.Finite.Quotient` `Mathlib.LinearAlgebra.FreeModule.IdealQuotient` `Mathlib.LinearAlgebra.FreeModule.Int` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.FreeModule.StrongRankCondition` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.LinearAlgebra.GeneralLinearGroup` `Mathlib.LinearAlgebra.Goursat` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.LinearAlgebra.Isomorphisms` `Mathlib.LinearAlgebra.Lagrange` `Mathlib.LinearAlgebra.LinearIndependent.Basic` `Mathlib.LinearAlgebra.LinearIndependent.Defs` `Mathlib.LinearAlgebra.LinearIndependent.Lemmas` `Mathlib.LinearAlgebra.LinearPMap` `Mathlib.LinearAlgebra.Matrix.AbsoluteValue` `Mathlib.LinearAlgebra.Matrix.Adjugate` `Mathlib.LinearAlgebra.Matrix.BaseChange` `Mathlib.LinearAlgebra.Matrix.Basis` `Mathlib.LinearAlgebra.Matrix.BilinearForm` `Mathlib.LinearAlgebra.Matrix.Block` `Mathlib.LinearAlgebra.Matrix.Charpoly.Basic` `Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField` `Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.LinearAlgebra.Matrix.Charpoly.Univ` `Mathlib.LinearAlgebra.Matrix.Circulant` `Mathlib.LinearAlgebra.Matrix.Determinant.Basic` `Mathlib.LinearAlgebra.Matrix.Determinant.Misc` `Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.LinearAlgebra.Matrix.DotProduct` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.LinearAlgebra.Matrix.FiniteDimensional` `Mathlib.LinearAlgebra.Matrix.FixedDetMatrices` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.LinearAlgebra.Matrix.IsDiag` `Mathlib.LinearAlgebra.Matrix.MvPolynomial` `Mathlib.LinearAlgebra.Matrix.Nondegenerate` `Mathlib.LinearAlgebra.Matrix.NonsingularInverse` `Mathlib.LinearAlgebra.Matrix.Orthogonal` `Mathlib.LinearAlgebra.Matrix.Permanent` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.Matrix.Polynomial` `Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup` `Mathlib.LinearAlgebra.Matrix.Reindex` `Mathlib.LinearAlgebra.Matrix.SemiringInverse` `Mathlib.LinearAlgebra.Matrix.SesquilinearForm` `Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.LinearAlgebra.Matrix.Swap` `Mathlib.LinearAlgebra.Matrix.Symmetric` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.LinearAlgebra.Matrix.ToLinearEquiv` `Mathlib.LinearAlgebra.Matrix.Trace` `Mathlib.LinearAlgebra.Matrix.Transvection` `Mathlib.LinearAlgebra.Matrix.Unique` `Mathlib.LinearAlgebra.Matrix.ZPow` `Mathlib.LinearAlgebra.Multilinear.Basic` `Mathlib.LinearAlgebra.Multilinear.Basis` `Mathlib.LinearAlgebra.Multilinear.Curry` `Mathlib.LinearAlgebra.Multilinear.DFinsupp` `Mathlib.LinearAlgebra.Multilinear.FiniteDimensional` `Mathlib.LinearAlgebra.Multilinear.Pi` `Mathlib.LinearAlgebra.Multilinear.TensorProduct` `Mathlib.LinearAlgebra.Orientation` `Mathlib.LinearAlgebra.PID` `Mathlib.LinearAlgebra.PerfectPairing.Basic` `Mathlib.LinearAlgebra.PerfectPairing.Restrict` `Mathlib.LinearAlgebra.PiTensorProduct` `Mathlib.LinearAlgebra.Pi` `Mathlib.LinearAlgebra.Prod` `Mathlib.LinearAlgebra.Projection` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.LinearAlgebra.QuadraticForm.Basic` `Mathlib.LinearAlgebra.QuadraticForm.Basis` `Mathlib.LinearAlgebra.QuadraticForm.Dual` `Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv` `Mathlib.LinearAlgebra.QuadraticForm.Isometry` `Mathlib.LinearAlgebra.QuadraticForm.Prod` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct` `Mathlib.LinearAlgebra.Quotient.Basic` `Mathlib.LinearAlgebra.Quotient.Defs` `Mathlib.LinearAlgebra.Quotient.Pi` `Mathlib.LinearAlgebra.Ray` `Mathlib.LinearAlgebra.SModEq` `Mathlib.LinearAlgebra.SesquilinearForm` `Mathlib.LinearAlgebra.Span.Basic` `Mathlib.LinearAlgebra.Span.Defs` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basic` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basis` `Mathlib.LinearAlgebra.SymplecticGroup` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Basis` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.LinearAlgebra.TensorPower.Basic` `Mathlib.LinearAlgebra.TensorPower.Pairing` `Mathlib.LinearAlgebra.TensorProduct.Associator` `Mathlib.LinearAlgebra.TensorProduct.Basic` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.LinearAlgebra.TensorProduct.Graded.External` `Mathlib.LinearAlgebra.TensorProduct.Graded.Internal` `Mathlib.LinearAlgebra.TensorProduct.Matrix` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.LinearAlgebra.TensorProduct.Pi` `Mathlib.LinearAlgebra.TensorProduct.Prod` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.LinearAlgebra.TensorProduct.Tower` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.LinearAlgebra.Trace` `Mathlib.LinearAlgebra.UnitaryGroup` `Mathlib.LinearAlgebra.Vandermonde` `Mathlib.Logic.Godel.GodelBetaFunction` `Mathlib.Logic.Hydra` `Mathlib.MeasureTheory.Constructions.AddChar` `Mathlib.MeasureTheory.Constructions.Cylinders` `Mathlib.MeasureTheory.Constructions.SubmoduleQuotient` `Mathlib.MeasureTheory.MeasurableSpace.Basic` `Mathlib.MeasureTheory.MeasurableSpace.Card` `Mathlib.MeasureTheory.MeasurableSpace.Constructions` `Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated` `Mathlib.MeasureTheory.MeasurableSpace.Embedding` `Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated` `Mathlib.MeasureTheory.MeasurableSpace.NCard` `Mathlib.MeasureTheory.MeasurableSpace.Pi` `Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict` `Mathlib.MeasureTheory.MeasurableSpace.Prod` `Mathlib.MeasureTheory.PiSystem` `Mathlib.MeasureTheory.SetAlgebra` `Mathlib.MeasureTheory.SetSemiring` `Mathlib.ModelTheory.Algebra.Field.Basic` `Mathlib.ModelTheory.Algebra.Field.CharP` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed` `Mathlib.ModelTheory.Algebra.Ring.Basic` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.ModelTheory.Basic` `Mathlib.ModelTheory.Bundled` `Mathlib.ModelTheory.Complexity` `Mathlib.ModelTheory.Definability` `Mathlib.ModelTheory.DirectLimit` `Mathlib.ModelTheory.ElementaryMaps` `Mathlib.ModelTheory.ElementarySubstructures` `Mathlib.ModelTheory.Encoding` `Mathlib.ModelTheory.Equivalence` `Mathlib.ModelTheory.FinitelyGenerated` `Mathlib.ModelTheory.Graph` `Mathlib.ModelTheory.LanguageMap` `Mathlib.ModelTheory.PartialEquiv` `Mathlib.ModelTheory.Quotients` `Mathlib.ModelTheory.Satisfiability` `Mathlib.ModelTheory.Semantics` `Mathlib.ModelTheory.Skolem` `Mathlib.ModelTheory.Substructures` `Mathlib.ModelTheory.Syntax` `Mathlib.ModelTheory.Types` `Mathlib.ModelTheory.Ultraproducts` `Mathlib.NumberTheory.ADEInequality` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.NumberTheory.Basic` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue` `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.DirichletCharacter.Basic` `Mathlib.NumberTheory.Divisors` `Mathlib.NumberTheory.EllipticDivisibilitySequence` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.NumberTheory.FLT.Four` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.NumberTheory.FLT.Polynomial` `Mathlib.NumberTheory.FactorisationProperties` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.NumberTheory.Harmonic.Defs` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.NumberTheory.LegendreSymbol.Basic` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic` `Mathlib.NumberTheory.LegendreSymbol.ZModChar` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.LucasPrimality` `Mathlib.NumberTheory.MaricaSchoenheim` `Mathlib.NumberTheory.MulChar.Basic` `Mathlib.NumberTheory.Multiplicity` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.Padics.PadicNorm` `Mathlib.NumberTheory.Padics.PadicVal.Basic` `Mathlib.NumberTheory.Padics.PadicVal.Defs` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.NumberTheory.PrimeCounting` `Mathlib.NumberTheory.Primorial` `Mathlib.NumberTheory.PythagoreanTriples` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.SmoothNumbers` `Mathlib.NumberTheory.SumFourSquares` `Mathlib.NumberTheory.Wilson` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.Order.Atoms.Finite` `Mathlib.Order.Birkhoff` `Mathlib.Order.BooleanGenerators` `Mathlib.Order.BooleanSubalgebra` `Mathlib.Order.Category.FinBddDistLat` `Mathlib.Order.Category.FinBoolAlg` `Mathlib.Order.Category.FinPartOrd` `Mathlib.Order.Category.NonemptyFinLinOrd` `Mathlib.Order.Category.OmegaCompletePartialOrder` `Mathlib.Order.CompactlyGenerated.Basic` `Mathlib.Order.CompactlyGenerated.Intervals` `Mathlib.Order.CompleteLattice.Finset` `Mathlib.Order.CompleteLattice.SetLike` `Mathlib.Order.CompletePartialOrder` `Mathlib.Order.CompleteSublattice` `Mathlib.Order.ConditionallyCompleteLattice.Finset` `Mathlib.Order.Disjointed` `Mathlib.Order.Extension.Well` `Mathlib.Order.Filter.AtTopBot.BigOperators` `Mathlib.Order.Filter.AtTopBot.CountablyGenerated` `Mathlib.Order.Filter.AtTopBot.Finite` `Mathlib.Order.Filter.AtTopBot.Finset` `Mathlib.Order.Filter.AtTopBot.Floor` `Mathlib.Order.Filter.AtTopBot.Prod` `Mathlib.Order.Filter.Bases.Finite` `Mathlib.Order.Filter.CardinalInter` `Mathlib.Order.Filter.Cocardinal` `Mathlib.Order.Filter.Cofinite` `Mathlib.Order.Filter.CountablyGenerated` `Mathlib.Order.Filter.EventuallyConst` `Mathlib.Order.Filter.FilterProduct` `Mathlib.Order.Filter.Finite` `Mathlib.Order.Filter.Germ.Basic` `Mathlib.Order.Filter.Germ.OrderedMonoid` `Mathlib.Order.Filter.IndicatorFunction` `Mathlib.Order.Filter.Interval` `Mathlib.Order.Filter.IsBounded` `Mathlib.Order.Filter.Lift` `Mathlib.Order.Filter.Pi` `Mathlib.Order.Filter.Pointwise` `Mathlib.Order.Filter.Ring` `Mathlib.Order.Filter.SmallSets` `Mathlib.Order.Filter.Subsingleton` `Mathlib.Order.Filter.Ultrafilter.Basic` `Mathlib.Order.FixedPoints` `Mathlib.Order.GameAdd` `Mathlib.Order.Height` `Mathlib.Order.Interval.Finset.Basic` `Mathlib.Order.Interval.Finset.Box` `Mathlib.Order.Interval.Finset.Defs` `Mathlib.Order.Interval.Finset.Fin` `Mathlib.Order.Interval.Finset.Nat` `Mathlib.Order.Interval.Finset.SuccPred` `Mathlib.Order.Interval.Multiset` `Mathlib.Order.Interval.Set.Final` `Mathlib.Order.Interval.Set.OrdConnectedLinear` `Mathlib.Order.JordanHolder` `Mathlib.Order.KonigLemma` `Mathlib.Order.KrullDimension` `Mathlib.Order.LiminfLimsup` `Mathlib.Order.Monotone.MonovaryOrder` `Mathlib.Order.OmegaCompletePartialOrder` `Mathlib.Order.OrderIsoNat` `Mathlib.Order.PartialSups` `Mathlib.Order.Partition.Basic` `Mathlib.Order.Partition.Equipartition` `Mathlib.Order.Partition.Finpartition` `Mathlib.Order.RelSeries` `Mathlib.Order.Restriction` `Mathlib.Order.Sublattice` `Mathlib.Order.SuccPred.LinearLocallyFinite` `Mathlib.Order.SupClosed` `Mathlib.Order.SupIndep` `Mathlib.Order.UpperLower.LocallyFinite` `Mathlib.Order.WellFoundedSet` `Mathlib.Order.WellQuasiOrder` `Mathlib.Probability.Kernel.IonescuTulcea.Maps` `Mathlib.RepresentationTheory.Basic` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.Coinduced` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.GroupCohomology.Basic` `Mathlib.RepresentationTheory.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.GroupCohomology.Resolution` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RepresentationTheory.Maschke` `Mathlib.RepresentationTheory.Rep` `Mathlib.RepresentationTheory.Submodule` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.LocalRing` `Mathlib.RingTheory.AdicCompletion.Noetherian` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.RingTheory.Adjoin.FG` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.RingTheory.Adjoin.Polynomial` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.RingTheory.Adjoin.Tower` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.RingTheory.AlgebraTower` `Mathlib.RingTheory.Algebraic.Basic` `Mathlib.RingTheory.Algebraic.Cardinality` `Mathlib.RingTheory.Algebraic.Defs` `Mathlib.RingTheory.Algebraic.Integral` `Mathlib.RingTheory.Algebraic.LinearIndependent` `Mathlib.RingTheory.Algebraic.MvPolynomial` `Mathlib.RingTheory.Algebraic.Pi` `Mathlib.RingTheory.AlgebraicIndependent.Adjoin` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.AlgebraicIndependent.Basic` `Mathlib.RingTheory.AlgebraicIndependent.Defs` `Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality` `Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis` `Mathlib.RingTheory.AlgebraicIndependent.Transcendental` `Mathlib.RingTheory.Artinian.Algebra` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.Bezout` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.Bialgebra.MonoidAlgebra` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.RingTheory.ChainOfDivisors` `Mathlib.RingTheory.ClassGroup` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.RingTheory.Coalgebra.MonoidAlgebra` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.RingTheory.Complex` `Mathlib.RingTheory.Congruence.BigOperators` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.RingTheory.Coprime.Lemmas` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.Ideal` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.RingTheory.Derivation.Lie` `Mathlib.RingTheory.Derivation.MapCoeffs` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.DividedPowers.Basic` `Mathlib.RingTheory.DividedPowers.DPMorphism` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.EssentialFiniteness` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.FilteredAlgebra.Basic` `Mathlib.RingTheory.Filtration` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.FinitePresentation` `Mathlib.RingTheory.FiniteStability` `Mathlib.RingTheory.FiniteType` `Mathlib.RingTheory.Finiteness.Basic` `Mathlib.RingTheory.Finiteness.Bilinear` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.RingTheory.Finiteness.Defs` `Mathlib.RingTheory.Finiteness.Finsupp` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.RingTheory.Finiteness.Lattice` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.Finiteness.Prod` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.RingTheory.Finiteness.Quotient` `Mathlib.RingTheory.Finiteness.Small` `Mathlib.RingTheory.Finiteness.Subalgebra` `Mathlib.RingTheory.Fintype` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.FractionalIdeal.Operations` `Mathlib.RingTheory.FreeCommRing` `Mathlib.RingTheory.FreeRing` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.GradedAlgebra.FiniteType` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.HahnSeries.Addition` `Mathlib.RingTheory.HahnSeries.Basic` `Mathlib.RingTheory.HahnSeries.HEval` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.HopfAlgebra.Basic` `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra` `Mathlib.RingTheory.HopfAlgebra.TensorProduct` `Mathlib.RingTheory.Ideal.AssociatedPrime.Basic` `Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness` `Mathlib.RingTheory.Ideal.AssociatedPrime` `Mathlib.RingTheory.Ideal.Basic` `Mathlib.RingTheory.Ideal.Basis` `Mathlib.RingTheory.Ideal.BigOperators` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.RingTheory.Ideal.Defs` `Mathlib.RingTheory.Ideal.GoingUp` `Mathlib.RingTheory.Ideal.Height` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.Ideal.Lattice` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.RingTheory.Ideal.Maximal` `Mathlib.RingTheory.Ideal.MinimalPrime.Basic` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.Ideal.Nonunits` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Ideal.Over` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Prime` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.RingTheory.Ideal.Quotient.Basic` `Mathlib.RingTheory.Ideal.Quotient.Defs` `Mathlib.RingTheory.Ideal.Quotient.Index` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.RingTheory.Ideal.Quotient.PowTransition` `Mathlib.RingTheory.Ideal.Span` `Mathlib.RingTheory.Idempotents` `Mathlib.RingTheory.Int.Basic` `Mathlib.RingTheory.IntegralClosure.Algebra.Basic` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.RingTheory.IntegralDomain` `Mathlib.RingTheory.Invariant` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.Jacobson.Polynomial` `Mathlib.RingTheory.Jacobson.Radical` `Mathlib.RingTheory.Jacobson.Ring` `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.KrullDimension.Module` `Mathlib.RingTheory.KrullDimension.NonZeroDivisors` `Mathlib.RingTheory.KrullDimension.Zero` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.Length` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalProperties.Projective` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.Basic` `Mathlib.RingTheory.LocalRing.LocalSubring` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs` `Mathlib.RingTheory.LocalRing.NonLocalRing` `Mathlib.RingTheory.LocalRing.Quotient` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.RingTheory.LocalRing.Subring` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.RingTheory.Localization.Basic` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.RingTheory.Localization.Defs` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.Localization.Free` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Localization.Integer` `Mathlib.RingTheory.Localization.Integral` `Mathlib.RingTheory.Localization.InvSubmonoid` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.Localization.Module` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.RingTheory.Localization.Pi` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.RingTheory.MatrixAlgebra` `Mathlib.RingTheory.MatrixPolynomialAlgebra` `Mathlib.RingTheory.Morita.Basic` `Mathlib.RingTheory.Multiplicity` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.RingTheory.MvPolynomial.EulerIdentity` `Mathlib.RingTheory.MvPolynomial.FreeCommRing` `Mathlib.RingTheory.MvPolynomial.Groebner` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex` `Mathlib.RingTheory.MvPolynomial.MonomialOrder` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.RingTheory.MvPolynomial` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.RingTheory.MvPowerSeries.Order` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Nilpotent.Basic` `Mathlib.RingTheory.Nilpotent.Defs` `Mathlib.RingTheory.Nilpotent.Exp` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.RingTheory.NoetherNormalization` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.RingTheory.Noetherian.Defs` `Mathlib.RingTheory.Noetherian.Filter` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.RingTheory.NonUnitalSubring.Basic` `Mathlib.RingTheory.NonUnitalSubsemiring.Basic` `Mathlib.RingTheory.Norm.Basic` `Mathlib.RingTheory.Norm.Defs` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.NormTrace` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.OreLocalization.Cardinality` `Mathlib.RingTheory.OreLocalization.Ring` `Mathlib.RingTheory.OrzechProperty` `Mathlib.RingTheory.PiTensorProduct` `Mathlib.RingTheory.Polynomial.Basic` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.RingTheory.Polynomial.Chebyshev` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.Polynomial.Dickson` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.RingTheory.Polynomial.Eisenstein.Criterion` `Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.RingTheory.Polynomial.HilbertPoly` `Mathlib.RingTheory.Polynomial.Ideal` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.RingTheory.Polynomial.IrreducibleRing` `Mathlib.RingTheory.Polynomial.Nilpotent` `Mathlib.RingTheory.Polynomial.Opposites` `Mathlib.RingTheory.Polynomial.Pochhammer` `Mathlib.RingTheory.Polynomial.Quotient` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.RingTheory.Polynomial.SeparableDegree` `Mathlib.RingTheory.Polynomial.SmallDegreeVieta` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.RingTheory.Polynomial.UniqueFactorization` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.RingTheory.PolynomialLaw.Basic` `Mathlib.RingTheory.PowerBasis` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.PowerSeries.CoeffMulMem` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.RingTheory.PowerSeries.NoZeroDivisors` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.RingTheory.Prime` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.Radical` `Mathlib.RingTheory.ReesAlgebra` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.RootsOfUnity.Basic` `Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.RingTheory.SimpleModule.Rank` `Mathlib.RingTheory.SimpleRing.Basic` `Mathlib.RingTheory.SimpleRing.Congr` `Mathlib.RingTheory.SimpleRing.Defs` `Mathlib.RingTheory.SimpleRing.Field` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.RingTheory.Spectrum.Maximal.Basic` `Mathlib.RingTheory.Spectrum.Maximal.Defs` `Mathlib.RingTheory.Spectrum.Maximal.Localization` `Mathlib.RingTheory.Spectrum.Maximal.Topology` `Mathlib.RingTheory.Spectrum.Prime.Basic` `Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet` `Mathlib.RingTheory.Spectrum.Prime.Defs` `Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC` `Mathlib.RingTheory.Spectrum.Prime.Jacobson` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Spectrum.Prime.Noetherian` `Mathlib.RingTheory.Spectrum.Prime.RingHom` `Mathlib.RingTheory.Spectrum.Prime.TensorProduct` `Mathlib.RingTheory.Spectrum.Prime.Topology` `Mathlib.RingTheory.Support` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.RingTheory.TensorProduct.IsBaseChangePi` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.RingTheory.TensorProduct.Pi` `Mathlib.RingTheory.TensorProduct.Quotient` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Defs` `Mathlib.RingTheory.TwoSidedIdeal.Basic` `Mathlib.RingTheory.TwoSidedIdeal.BigOperators` `Mathlib.RingTheory.TwoSidedIdeal.Instances` `Mathlib.RingTheory.TwoSidedIdeal.Kernel` `Mathlib.RingTheory.TwoSidedIdeal.Lattice` `Mathlib.RingTheory.TwoSidedIdeal.Operations` `Mathlib.RingTheory.UniqueFactorizationDomain.Basic` `Mathlib.RingTheory.UniqueFactorizationDomain.Defs` `Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet` `Mathlib.RingTheory.UniqueFactorizationDomain.Finite` `Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp` `Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity` `Mathlib.RingTheory.UniqueFactorizationDomain.Nat` `Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.RingTheory.Valuation.Extension` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.RingTheory.Valuation.LocalSubring` `Mathlib.RingTheory.Valuation.Minpoly` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValExtension` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.Defs` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.Domain` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Frobenius` `Mathlib.RingTheory.WittVector.Identities` `Mathlib.RingTheory.WittVector.InitTail` `Mathlib.RingTheory.WittVector.IsPoly` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.RingTheory.WittVector.MulCoeff` `Mathlib.RingTheory.WittVector.MulP` `Mathlib.RingTheory.WittVector.StructurePolynomial` `Mathlib.RingTheory.WittVector.Teichmuller` `Mathlib.RingTheory.WittVector.Truncated` `Mathlib.RingTheory.WittVector.Verschiebung` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.RingTheory.ZMod` `Mathlib.SetTheory.Cardinal.Aleph` `Mathlib.SetTheory.Cardinal.Arithmetic` `Mathlib.SetTheory.Cardinal.Basic` `Mathlib.SetTheory.Cardinal.Cofinality` `Mathlib.SetTheory.Cardinal.Continuum` `Mathlib.SetTheory.Cardinal.CountableCover` `Mathlib.SetTheory.Cardinal.Divisibility` `Mathlib.SetTheory.Cardinal.ENat` `Mathlib.SetTheory.Cardinal.Finite` `Mathlib.SetTheory.Cardinal.Finsupp` `Mathlib.SetTheory.Cardinal.Free` `Mathlib.SetTheory.Cardinal.HasCardinalLT` `Mathlib.SetTheory.Cardinal.NatCount` `Mathlib.SetTheory.Cardinal.Order` `Mathlib.SetTheory.Cardinal.Ordinal` `Mathlib.SetTheory.Cardinal.Pigeonhole` `Mathlib.SetTheory.Cardinal.Regular` `Mathlib.SetTheory.Cardinal.SchroederBernstein` `Mathlib.SetTheory.Cardinal.Subfield` `Mathlib.SetTheory.Cardinal.ToNat` `Mathlib.SetTheory.Cardinal.UnivLE` `Mathlib.SetTheory.Descriptive.Tree` `Mathlib.SetTheory.Game.Basic` `Mathlib.SetTheory.Game.Birthday` `Mathlib.SetTheory.Game.Domineering` `Mathlib.SetTheory.Game.Impartial` `Mathlib.SetTheory.Game.Nim` `Mathlib.SetTheory.Game.Ordinal` `Mathlib.SetTheory.Game.Short` `Mathlib.SetTheory.Game.State` `Mathlib.SetTheory.Nimber.Basic` `Mathlib.SetTheory.Nimber.Field` `Mathlib.SetTheory.Ordinal.Arithmetic` `Mathlib.SetTheory.Ordinal.Basic` `Mathlib.SetTheory.Ordinal.CantorNormalForm` `Mathlib.SetTheory.Ordinal.Enum` `Mathlib.SetTheory.Ordinal.Exponential` `Mathlib.SetTheory.Ordinal.Family` `Mathlib.SetTheory.Ordinal.FixedPointApproximants` `Mathlib.SetTheory.Ordinal.FixedPoint` `Mathlib.SetTheory.Ordinal.NaturalOps` `Mathlib.SetTheory.Ordinal.Notation` `Mathlib.SetTheory.Ordinal.Principal` `Mathlib.SetTheory.Ordinal.Rank` `Mathlib.SetTheory.Ordinal.Topology` `Mathlib.SetTheory.Ordinal.Veblen` `Mathlib.SetTheory.PGame.Algebra` `Mathlib.SetTheory.PGame.Order` `Mathlib.SetTheory.Surreal.Basic` `Mathlib.SetTheory.Surreal.Multiplication` `Mathlib.SetTheory.ZFC.Class` `Mathlib.SetTheory.ZFC.Ordinal` `Mathlib.SetTheory.ZFC.Rank` `Mathlib.Tactic.Algebraize` `Mathlib.Tactic.ComputeDegree` `Mathlib.Tactic.DeriveFintype` `Mathlib.Tactic.LinearCombination.Lemmas` `Mathlib.Tactic.LinearCombination` `Mathlib.Tactic.Module` `Mathlib.Tactic.NormNum.BigOperators` `Mathlib.Tactic.NormNum.IsCoprime` `Mathlib.Tactic.NormNum.NatFib` `Mathlib.Tactic.Polyrith` `Mathlib.Tactic.Positivity.Finset` `Mathlib.Tactic.Positivity` `Mathlib.Tactic.ReduceModChar` `Mathlib.Tactic.RewriteSearch` `Mathlib.Tactic.Rify` `Mathlib.Testing.Plausible.Functions` `Mathlib.Topology.AlexandrovDiscrete` `Mathlib.Topology.Algebra.Affine` `Mathlib.Topology.Algebra.Algebra.Rat` `Mathlib.Topology.Algebra.ConstMulAction` `Mathlib.Topology.Algebra.Constructions.DomMulAct` `Mathlib.Topology.Algebra.Constructions` `Mathlib.Topology.Algebra.ContinuousMonoidHom` `Mathlib.Topology.Algebra.Group.Defs` `Mathlib.Topology.Algebra.GroupWithZero` `Mathlib.Topology.Algebra.Indicator` `Mathlib.Topology.Algebra.InfiniteSum.Basic` `Mathlib.Topology.Algebra.InfiniteSum.Defs` `Mathlib.Topology.Algebra.Monoid.AddChar` `Mathlib.Topology.Algebra.Monoid.Defs` `Mathlib.Topology.Algebra.Monoid` `Mathlib.Topology.Algebra.MulAction` `Mathlib.Topology.Algebra.Order.Module` `Mathlib.Topology.Algebra.Order.Support` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.Topology.Algebra.ProperConstSMul` `Mathlib.Topology.Algebra.Semigroup` `Mathlib.Topology.Algebra.Star` `Mathlib.Topology.Algebra.Support` `Mathlib.Topology.Algebra.WithZeroTopology` `Mathlib.Topology.ApproximateUnit` `Mathlib.Topology.Baire.Lemmas` `Mathlib.Topology.Baire.LocallyCompactRegular` `Mathlib.Topology.Bases` `Mathlib.Topology.Bornology.Absorbs` `Mathlib.Topology.Bornology.Basic` `Mathlib.Topology.Bornology.Constructions` `Mathlib.Topology.Bornology.Hom` `Mathlib.Topology.Category.Born` `Mathlib.Topology.Category.CompHausLike.Basic` `Mathlib.Topology.Category.CompHausLike.EffectiveEpi` `Mathlib.Topology.Category.CompHausLike.Limits` `Mathlib.Topology.Category.CompHausLike.SigmaComparison` `Mathlib.Topology.Category.FinTopCat` `Mathlib.Topology.Category.Sequential` `Mathlib.Topology.Category.TopCat.Adjunctions` `Mathlib.Topology.Category.TopCat.Basic` `Mathlib.Topology.Category.TopCat.EffectiveEpi` `Mathlib.Topology.Category.TopCat.EpiMono` `Mathlib.Topology.Category.TopCat.Limits.Basic` `Mathlib.Topology.Category.TopCat.Limits.Cofiltered` `Mathlib.Topology.Category.TopCat.Limits.Konig` `Mathlib.Topology.Category.TopCat.Limits.Products` `Mathlib.Topology.Category.TopCat.Limits.Pullbacks` `Mathlib.Topology.Category.TopCat.OpenNhds` `Mathlib.Topology.Category.TopCat.Opens` `Mathlib.Topology.Category.TopCat.ULift` `Mathlib.Topology.Category.TopCat.Yoneda` `Mathlib.Topology.Category.UniformSpace` `Mathlib.Topology.ClopenBox` `Mathlib.Topology.Clopen` `Mathlib.Topology.Closure` `Mathlib.Topology.ClusterPt` `Mathlib.Topology.Coherent` `Mathlib.Topology.CompactOpen` `Mathlib.Topology.Compactification.OnePointEquiv` `Mathlib.Topology.Compactification.OnePoint` `Mathlib.Topology.Compactness.Bases` `Mathlib.Topology.Compactness.Compact` `Mathlib.Topology.Compactness.Exterior` `Mathlib.Topology.Compactness.Lindelof` `Mathlib.Topology.Compactness.LocallyCompact` `Mathlib.Topology.Compactness.LocallyFinite` `Mathlib.Topology.Compactness.Paracompact` `Mathlib.Topology.Compactness.SigmaCompact` `Mathlib.Topology.Connected.Basic` `Mathlib.Topology.Connected.Clopen` `Mathlib.Topology.Connected.LocallyConnected` `Mathlib.Topology.Connected.Separation` `Mathlib.Topology.Connected.TotallyDisconnected` `Mathlib.Topology.Constructible` `Mathlib.Topology.Constructions.SumProd` `Mathlib.Topology.Constructions` `Mathlib.Topology.ContinuousMap.Basic` `Mathlib.Topology.ContinuousMap.CocompactMap` `Mathlib.Topology.ContinuousMap.Interval` `Mathlib.Topology.ContinuousMap.Ordered` `Mathlib.Topology.ContinuousMap.SecondCountableSpace` `Mathlib.Topology.ContinuousMap.Sigma` `Mathlib.Topology.ContinuousMap.T0Sierpinski` `Mathlib.Topology.ContinuousOn` `Mathlib.Topology.Continuous` `Mathlib.Topology.Covering` `Mathlib.Topology.DenseEmbedding` `Mathlib.Topology.DerivedSet` `Mathlib.Topology.DiscreteQuotient` `Mathlib.Topology.DiscreteSubset` `Mathlib.Topology.ExtendFrom` `Mathlib.Topology.Exterior` `Mathlib.Topology.ExtremallyDisconnected` `Mathlib.Topology.FiberBundle.Basic` `Mathlib.Topology.FiberBundle.Constructions` `Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle` `Mathlib.Topology.FiberBundle.Trivialization` `Mathlib.Topology.FiberPartition` `Mathlib.Topology.Filter` `Mathlib.Topology.GDelta.Basic` `Mathlib.Topology.Gluing` `Mathlib.Topology.Hom.ContinuousEvalConst` `Mathlib.Topology.Hom.ContinuousEval` `Mathlib.Topology.Hom.Open` `Mathlib.Topology.Homeomorph.Defs` `Mathlib.Topology.Homeomorph.Lemmas` `Mathlib.Topology.IndicatorConstPointwise` `Mathlib.Topology.Inseparable` `Mathlib.Topology.Instances.Discrete` `Mathlib.Topology.Instances.ENat` `Mathlib.Topology.Instances.Shrink` `Mathlib.Topology.Instances.Sign` `Mathlib.Topology.Instances.ZMod` `Mathlib.Topology.Irreducible` `Mathlib.Topology.IsClosedRestrict` `Mathlib.Topology.IsLocalHomeomorph` `Mathlib.Topology.JacobsonSpace` `Mathlib.Topology.KrullDimension` `Mathlib.Topology.List` `Mathlib.Topology.LocalAtTarget` `Mathlib.Topology.LocallyClosed` `Mathlib.Topology.LocallyConstant.Algebra` `Mathlib.Topology.LocallyConstant.Basic` `Mathlib.Topology.LocallyFinite` `Mathlib.Topology.Maps.Basic` `Mathlib.Topology.Maps.OpenQuotient` `Mathlib.Topology.Maps.Proper.Basic` `Mathlib.Topology.Maps.Proper.UniversallyClosed` `Mathlib.Topology.MetricSpace.BundledFun` `Mathlib.Topology.Neighborhoods` `Mathlib.Topology.NhdsSet` `Mathlib.Topology.NoetherianSpace` `Mathlib.Topology.OmegaCompletePartialOrder` `Mathlib.Topology.Order.Basic` `Mathlib.Topology.Order.Bornology` `Mathlib.Topology.Order.Category.AlexDisc` `Mathlib.Topology.Order.Compact` `Mathlib.Topology.Order.CountableSeparating` `Mathlib.Topology.Order.DenselyOrdered` `Mathlib.Topology.Order.ExtendFrom` `Mathlib.Topology.Order.ExtrClosure` `Mathlib.Topology.Order.Filter` `Mathlib.Topology.Order.Hom.Basic` `Mathlib.Topology.Order.Hom.Esakia` `Mathlib.Topology.Order.IntermediateValue` `Mathlib.Topology.Order.IsLUB` `Mathlib.Topology.Order.IsLocallyClosed` `Mathlib.Topology.Order.Lattice` `Mathlib.Topology.Order.LawsonTopology` `Mathlib.Topology.Order.LeftRightLim` `Mathlib.Topology.Order.LeftRightNhds` `Mathlib.Topology.Order.LeftRight` `Mathlib.Topology.Order.LocalExtr` `Mathlib.Topology.Order.LowerUpperTopology` `Mathlib.Topology.Order.MonotoneContinuity` `Mathlib.Topology.Order.MonotoneConvergence` `Mathlib.Topology.Order.Monotone` `Mathlib.Topology.Order.NhdsSet` `Mathlib.Topology.Order.OrderClosedExtr` `Mathlib.Topology.Order.OrderClosed` `Mathlib.Topology.Order.PartialSups` `Mathlib.Topology.Order.Priestley` `Mathlib.Topology.Order.ProjIcc` `Mathlib.Topology.Order.Rolle` `Mathlib.Topology.Order.ScottTopology` `Mathlib.Topology.Order.T5` `Mathlib.Topology.Order.UpperLowerSetTopology` `Mathlib.Topology.Order` `Mathlib.Topology.PartialHomeomorph` `Mathlib.Topology.Partial` `Mathlib.Topology.Perfect` `Mathlib.Topology.Piecewise` `Mathlib.Topology.PreorderRestrict` `Mathlib.Topology.QuasiSeparated` `Mathlib.Topology.SeparatedMap` `Mathlib.Topology.Separation.Basic` `Mathlib.Topology.Separation.Connected` `Mathlib.Topology.Separation.CountableSeparatingOn` `Mathlib.Topology.Separation.DisjointCover` `Mathlib.Topology.Separation.GDelta` `Mathlib.Topology.Separation.Hausdorff` `Mathlib.Topology.Separation.Profinite` `Mathlib.Topology.Separation.Regular` `Mathlib.Topology.Separation.SeparatedNhds` `Mathlib.Topology.Sequences` `Mathlib.Topology.Sets.Closeds` `Mathlib.Topology.Sets.Compacts` `Mathlib.Topology.Sets.OpenCover` `Mathlib.Topology.Sets.Opens` `Mathlib.Topology.Sets.Order` `Mathlib.Topology.Sheaves.Alexandrov` `Mathlib.Topology.Sheaves.Forget` `Mathlib.Topology.Sheaves.Functors` `Mathlib.Topology.Sheaves.Limits` `Mathlib.Topology.Sheaves.LocalPredicate` `Mathlib.Topology.Sheaves.LocallySurjective` `Mathlib.Topology.Sheaves.MayerVietoris` `Mathlib.Topology.Sheaves.PUnit` `Mathlib.Topology.Sheaves.PresheafOfFunctions` `Mathlib.Topology.Sheaves.Presheaf` `Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts` `Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover` `Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections` `Mathlib.Topology.Sheaves.SheafCondition.Sites` `Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing` `Mathlib.Topology.Sheaves.SheafOfFunctions` `Mathlib.Topology.Sheaves.Sheaf` `Mathlib.Topology.Sheaves.Sheafify` `Mathlib.Topology.Sheaves.Skyscraper` `Mathlib.Topology.Sheaves.Stalks` `Mathlib.Topology.ShrinkingLemma` `Mathlib.Topology.Sober` `Mathlib.Topology.Specialization` `Mathlib.Topology.Spectral.Basic` `Mathlib.Topology.Spectral.Hom` `Mathlib.Topology.Spectral.Prespectral` `Mathlib.Topology.StoneCech` `Mathlib.Topology.Ultrafilter` `Mathlib.Topology.UniformSpace.AbsoluteValue` `Mathlib.Topology.UniformSpace.AbstractCompletion` `Mathlib.Topology.UniformSpace.Ascoli` `Mathlib.Topology.UniformSpace.Basic` `Mathlib.Topology.UniformSpace.Cauchy` `Mathlib.Topology.UniformSpace.CompactConvergence` `Mathlib.Topology.UniformSpace.Compact` `Mathlib.Topology.UniformSpace.CompleteSeparated` `Mathlib.Topology.UniformSpace.Completion` `Mathlib.Topology.UniformSpace.Defs` `Mathlib.Topology.UniformSpace.Equicontinuity` `Mathlib.Topology.UniformSpace.Equiv` `Mathlib.Topology.UniformSpace.HeineCantor` `Mathlib.Topology.UniformSpace.LocallyUniformConvergence` `Mathlib.Topology.UniformSpace.OfCompactT2` `Mathlib.Topology.UniformSpace.OfFun` `Mathlib.Topology.UniformSpace.Pi` `Mathlib.Topology.UniformSpace.Separation` `Mathlib.Topology.UniformSpace.Ultra.Basic` `Mathlib.Topology.UniformSpace.Ultra.Constructions` `Mathlib.Topology.UniformSpace.UniformApproximation` `Mathlib.Topology.UniformSpace.UniformConvergenceTopology` `Mathlib.Topology.UniformSpace.UniformConvergence` `Mathlib.Topology.UniformSpace.UniformEmbedding`	1
29 files `Mathlib.Algebra.Group.Action.Pointwise.Set.Basic` `Mathlib.Algebra.Group.Pointwise.Set.Basic` `Mathlib.Algebra.Group.Pointwise.Set.Lattice` `Mathlib.Algebra.Group.Pointwise.Set.Scalar` `Mathlib.Algebra.Group.Submonoid.Operations` `Mathlib.Algebra.Group.Subsemigroup.Operations` `Mathlib.Algebra.GroupWithZero.Action.Prod` `Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic` `Mathlib.Algebra.GroupWithZero.Prod` `Mathlib.Algebra.Module.PointwisePi` `Mathlib.Algebra.Module.Prod` `Mathlib.Algebra.Order.Field.Pointwise` `Mathlib.Algebra.Order.Group.Action.Flag` `Mathlib.Algebra.Order.Group.Pointwise.Bounds` `Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice` `Mathlib.Algebra.Order.Group.Prod` `Mathlib.Algebra.Order.Kleene` `Mathlib.Algebra.Order.Monoid.Prod` `Mathlib.Algebra.Order.Ring.Prod` `Mathlib.Algebra.Ring.Action.Pointwise.Set` `Mathlib.Algebra.Ring.Pointwise.Set` `Mathlib.Algebra.Ring.Prod` `Mathlib.GroupTheory.Congruence.Basic` `Mathlib.GroupTheory.GroupAction.Pointwise` `Mathlib.GroupTheory.GroupAction.Support` `Mathlib.GroupTheory.Submonoid.Center` `Mathlib.GroupTheory.Submonoid.Centralizer` `Mathlib.RingTheory.Congruence.Basic` `Mathlib.RingTheory.Congruence.Opposite`	2
4 files `Mathlib.Algebra.Group.Action.Prod` `Mathlib.Algebra.Group.Prod` `Mathlib.Data.Int.Cast.Prod` `Mathlib.Data.Nat.Cast.Prod`	9

Declarations diff

+ IsAddTorsionFree.of_noZeroSMulDivisors_int
+ IsAddTorsionFree.of_noZeroSMulDivisors_nat
+ IsAddTorsionFree.to_noZeroSMulDivisors_int
+ IsAddTorsionFree.to_noZeroSMulDivisors_nat
+ IsMulTorsionFree.of_not_isOfFinOrder
+ Subsingleton.to_isMulTorsionFree
+ instance _root_.QuotientGroup.instIsMulTorsionFree : IsMulTorsionFree <| G ⧸ torsion G := by
+ isMulTorsionFree_iff_not_isOfFinOrder
+ isMulTorsionFree_iff_torsion_eq_bot
+ noZeroSMulDivisors_int_iff_isAddTorsionFree
+ noZeroSMulDivisors_nat_iff_isAddTorsionFree
+ not_isMulTorsionFree_iff_isOfFinOrder
+ not_isMulTorsionFree_of_isTorsion
+ not_isOfFinOrder_of_isMulTorsionFree
+ not_isTorsion_of_isMulTorsionFree
+++ _
+++ instIsMulTorsionFree

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/GroupTheory/OrderOfElement.lean

grunweg · 2025-05-08T07:12:39Z

The auto-assignment algorithm proposed a reviewer; let me manually override this and assign b-mehta who has been reviewing already.

b-mehta

This looks reasonable to me, with the caveat that I'm not convinced it's a good idea to import Algebra.Group.Torsion in Algebra.Group.Subgroup.Basic and Algebra.Group.Prod: certainly the product group and the notion of subgroup feel more elementary than the notion of torsion. So for now, I'll

maintainer merge

Mathlib/Algebra/Group/Pi/Lemmas.lean

Mathlib/GroupTheory/Torsion.lean

github-actions · 2025-05-13T17:05:16Z

🚀 Pull request has been placed on the maintainer queue by b-mehta.

jcommelin

Thanks 🎉

bors merge

The new imports just come from making `#min_imports` and `mk_iff` available earlier. From Toric

mathlib-bors · 2025-05-14T08:26:46Z

Pull request successfully merged into master.

Build succeeded:

The new imports just come from making `#min_imports` and `mk_iff` available earlier. From Toric

) The new imports just come from making `#min_imports` and `mk_iff` available earlier. From Toric

feat: more lemmas about torsion-free monoids

b285046

From Toric

YaelDillies added t-algebra Algebra (groups, rings, fields, etc) toric Part of the ongoing formalisation of toric varieties labels Apr 23, 2025

YaelDillies mentioned this pull request Apr 23, 2025

[Merged by Bors] - chore: replace Monoid.IsTorsionFree with IsMulTorsionFree #24311

Closed

1 task

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Apr 23, 2025

shake

1ab3693

b-mehta reviewed May 3, 2025

View reviewed changes

Mathlib/GroupTheory/OrderOfElement.lean Show resolved Hide resolved

grunweg assigned b-mehta May 8, 2025

b-mehta reviewed May 13, 2025

View reviewed changes

Mathlib/Algebra/Group/Pi/Lemmas.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/Torsion.lean Outdated Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 13, 2025

nits

f84d401

jcommelin reviewed May 14, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 14, 2025

mathlib-bors bot pushed a commit that referenced this pull request May 14, 2025

feat: more lemmas about torsion-free monoids (#24312)

753ef7e

The new imports just come from making `#min_imports` and `mk_iff` available earlier. From Toric

mathlib-bors bot changed the title ~~feat: more lemmas about torsion-free monoids~~ [Merged by Bors] - feat: more lemmas about torsion-free monoids May 14, 2025

mathlib-bors bot closed this May 14, 2025

mathlib-bors bot deleted the more_torsion_free_lemma branch May 14, 2025 08:26

jano-wol pushed a commit that referenced this pull request May 16, 2025

feat: more lemmas about torsion-free monoids (#24312)

a2abd90

The new imports just come from making `#min_imports` and `mk_iff` available earlier. From Toric

bwehlin pushed a commit to bwehlin/mathlib4 that referenced this pull request May 31, 2025

feat: more lemmas about torsion-free monoids (leanprover-community#24312

59313e7

) The new imports just come from making `#min_imports` and `mk_iff` available earlier. From Toric

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: more lemmas about torsion-free monoids#24312

[Merged by Bors] - feat: more lemmas about torsion-free monoids#24312
YaelDillies wants to merge 3 commits intomasterfrom
more_torsion_free_lemma

YaelDillies commented Apr 23, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Apr 23, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

grunweg commented May 8, 2025

Uh oh!

b-mehta left a comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented May 13, 2025

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented May 14, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

YaelDillies commented Apr 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary f84d401cbc

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

grunweg commented May 8, 2025

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented May 13, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented May 14, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

YaelDillies commented Apr 23, 2025 •

edited

Loading

github-actions bot commented Apr 23, 2025 •

edited

Loading