[Merged by Bors] - refactor(Logic/Equiv/List): split by eric-wieser · Pull Request #23092 · leanprover-community/mathlib4

eric-wieser · 2025-03-19T10:46:31Z

The motivation here is to delay the import of sorting.

github-actions · 2025-03-19T10:47:27Z

PR summary 96ea62b47a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Equiv.List	481	465	-16 (-3.33%)
Mathlib.Data.Set.Countable	488	472	-16 (-3.28%)

Import changes for all files

Files	Import difference
9 files `Mathlib.Data.Set.Countable` `Mathlib.Logic.Equiv.Array` `Mathlib.Logic.Equiv.List` `Mathlib.MeasureTheory.MeasurableSpace.Defs` `Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable` `Mathlib.MeasureTheory.MeasurableSpace.Instances` `Mathlib.MeasureTheory.MeasurableSpace.Invariants` `Mathlib.Order.Filter.CountableInter` `Mathlib.Order.Filter.CountableSeparatingOn`	-16
15 files `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.MeasureTheory.PiSystem` `Mathlib.Order.Filter.AtTopBot.Archimedean` `Mathlib.Order.Filter.CountablyGenerated` `Mathlib.Order.Filter.EventuallyConst` `Mathlib.Order.Filter.Subsingleton` `Mathlib.Topology.Baire.Lemmas` `Mathlib.Topology.GDelta.Basic`	-7
3 files `Mathlib.MeasureTheory.Constructions.AddChar` `Mathlib.MeasureTheory.SetAlgebra` `Mathlib.MeasureTheory.SetSemiring`	-6
379 files `Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries` `Mathlib.Algebra.Group.ConjFinite` `Mathlib.Algebra.Group.Pointwise.Set.Card` `Mathlib.Algebra.Group.Subgroup.Finite` `Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card` `Mathlib.Algebra.Module.Card` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Normed.Group.Subgroup` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject` `Mathlib.CategoryTheory.Action.Continuous` `Mathlib.CategoryTheory.Adhesive` `Mathlib.CategoryTheory.CofilteredSystem` `Mathlib.CategoryTheory.Comma.CardinalArrow` `Mathlib.CategoryTheory.EffectiveEpi.Extensive` `Mathlib.CategoryTheory.Extensive` `Mathlib.CategoryTheory.Galois.Basic` `Mathlib.CategoryTheory.Galois.Decomposition` `Mathlib.CategoryTheory.Galois.Examples` `Mathlib.CategoryTheory.Galois.GaloisObjects` `Mathlib.CategoryTheory.Limits.SmallComplete` `Mathlib.CategoryTheory.Presentable.Basic` `Mathlib.CategoryTheory.Presentable.IsCardinalFiltered` `Mathlib.CategoryTheory.Presentable.Limits` `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.ConstantSheaf` `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.LeftExact` `Mathlib.CategoryTheory.Sites.LocallyBijective` `Mathlib.CategoryTheory.Sites.LocallyFullyFaithful` `Mathlib.CategoryTheory.Sites.LocallyInjective` `Mathlib.CategoryTheory.Sites.LocallySurjective` `Mathlib.CategoryTheory.Sites.PreservesLocallyBijective` `Mathlib.CategoryTheory.Sites.Pullback` `Mathlib.CategoryTheory.Sites.Subsheaf` `Mathlib.CategoryTheory.Subobject.HasCardinalLT` `Mathlib.Combinatorics.Hall.Basic` `Mathlib.Combinatorics.Hindman` `Mathlib.Combinatorics.SimpleGraph.Ends.Defs` `Mathlib.Combinatorics.SimpleGraph.Ends.Properties` `Mathlib.Combinatorics.SimpleGraph.Finsubgraph` `Mathlib.Computability.Encoding` `Mathlib.Data.Analysis.Filter` `Mathlib.Data.Analysis.Topology` `Mathlib.Data.Finite.Card` `Mathlib.Data.Finite.Perm` `Mathlib.Data.Fintype.Units` `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.Rank.Cardinal` `Mathlib.Data.Matroid.Rank.Finite` `Mathlib.Data.Matroid.Restrict` `Mathlib.Data.Matroid.Sum` `Mathlib.Data.Rat.Cardinal` `Mathlib.Data.Set.Card.Arithmetic` `Mathlib.Data.Set.Card` `Mathlib.Data.Setoid.Partition.Card` `Mathlib.Dynamics.FixedPoints.Topology` `Mathlib.Dynamics.Minimal` `Mathlib.GroupTheory.ClassEquation` `Mathlib.GroupTheory.CoprodI` `Mathlib.GroupTheory.Coset.Card` `Mathlib.GroupTheory.GroupAction.CardCommute` `Mathlib.GroupTheory.MonoidLocalization.Cardinality` `Mathlib.GroupTheory.OreLocalization.Cardinality` `Mathlib.GroupTheory.Perm.DomMulAct` `Mathlib.GroupTheory.Perm.Subgroup` `Mathlib.InformationTheory.Hamming` `Mathlib.MeasureTheory.Constructions.Cylinders` `Mathlib.MeasureTheory.Constructions.SubmoduleQuotient` `Mathlib.MeasureTheory.MeasurableSpace.Basic` `Mathlib.MeasureTheory.MeasurableSpace.Card` `Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated` `Mathlib.MeasureTheory.MeasurableSpace.Embedding` `Mathlib.MeasureTheory.MeasurableSpace.Pi` `Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict` `Mathlib.MeasureTheory.MeasurableSpace.Prod` `Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.ModelTheory.Algebra.Field.Basic` `Mathlib.ModelTheory.Algebra.Ring.Basic` `Mathlib.ModelTheory.Basic` `Mathlib.ModelTheory.Bundled` `Mathlib.ModelTheory.Complexity` `Mathlib.ModelTheory.Definability` `Mathlib.ModelTheory.ElementaryMaps` `Mathlib.ModelTheory.ElementarySubstructures` `Mathlib.ModelTheory.Encoding` `Mathlib.ModelTheory.Equivalence` `Mathlib.ModelTheory.Graph` `Mathlib.ModelTheory.LanguageMap` `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.Order.Extension.Well` `Mathlib.Order.Filter.AtTopBot.CountablyGenerated` `Mathlib.Order.Filter.CardinalInter` `Mathlib.Order.Filter.Cofinite` `Mathlib.Order.Filter.Ultrafilter.Basic` `Mathlib.Order.LiminfLimsup` `Mathlib.Probability.Kernel.IonescuTulcea.Maps` `Mathlib.RingTheory.OreLocalization.Cardinality` `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.HasCardinalLT` `Mathlib.SetTheory.Cardinal.NatCount` `Mathlib.SetTheory.Cardinal.Ordinal` `Mathlib.SetTheory.Cardinal.Pigeonhole` `Mathlib.SetTheory.Cardinal.Regular` `Mathlib.SetTheory.Cardinal.ToNat` `Mathlib.SetTheory.Cardinal.UnivLE` `Mathlib.SetTheory.Game.Birthday` `Mathlib.SetTheory.Game.Domineering` `Mathlib.SetTheory.Game.Nim` `Mathlib.SetTheory.Game.Ordinal` `Mathlib.SetTheory.Game.Short` `Mathlib.SetTheory.Game.State` `Mathlib.SetTheory.Nimber.Basic` `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.Veblen` `Mathlib.SetTheory.Surreal.Basic` `Mathlib.SetTheory.ZFC.Rank` `Mathlib.Topology.AlexandrovDiscrete` `Mathlib.Topology.Algebra.Algebra.Rat` `Mathlib.Topology.Algebra.ConstMulAction` `Mathlib.Topology.Algebra.Constructions.DomMulAct` `Mathlib.Topology.Algebra.Constructions` `Mathlib.Topology.Algebra.GroupWithZero` `Mathlib.Topology.Algebra.Indicator` `Mathlib.Topology.Algebra.InfiniteSum.Basic` `Mathlib.Topology.Algebra.InfiniteSum.Defs` `Mathlib.Topology.Algebra.Monoid` `Mathlib.Topology.Algebra.MulAction` `Mathlib.Topology.Algebra.Order.Archimedean` `Mathlib.Topology.Algebra.Order.Support` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.Topology.Algebra.ProperConstSMul` `Mathlib.Topology.Algebra.Semigroup` `Mathlib.Topology.Algebra.Star.Real` `Mathlib.Topology.Algebra.Star` `Mathlib.Topology.Algebra.Support` `Mathlib.Topology.Algebra.WithZeroTopology` `Mathlib.Topology.ApproximateUnit` `Mathlib.Topology.Bases` `Mathlib.Topology.Bornology.Absorbs` `Mathlib.Topology.Bornology.Basic` `Mathlib.Topology.Bornology.Constructions` `Mathlib.Topology.Bornology.Hom` `Mathlib.Topology.Bornology.Real` `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.ULift` `Mathlib.Topology.Category.TopCat.Yoneda` `Mathlib.Topology.Category.UniformSpace` `Mathlib.Topology.Clopen` `Mathlib.Topology.CompactOpen` `Mathlib.Topology.Compactness.Compact` `Mathlib.Topology.Compactness.Exterior` `Mathlib.Topology.Compactness.Lindelof` `Mathlib.Topology.Compactness.LocallyCompact` `Mathlib.Topology.Compactness.Paracompact` `Mathlib.Topology.Compactness.PseudometrizableLindelof` `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.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.ContinuousOn` `Mathlib.Topology.DenseEmbedding` `Mathlib.Topology.DerivedSet` `Mathlib.Topology.DiscreteSubset` `Mathlib.Topology.EMetricSpace.Basic` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.EMetricSpace.Diam` `Mathlib.Topology.EMetricSpace.Lipschitz` `Mathlib.Topology.EMetricSpace.Pi` `Mathlib.Topology.ExtendFrom` `Mathlib.Topology.Exterior` `Mathlib.Topology.ExtremallyDisconnected` `Mathlib.Topology.Filter` `Mathlib.Topology.GDelta.UniformSpace` `Mathlib.Topology.Hom.ContinuousEvalConst` `Mathlib.Topology.Hom.ContinuousEval` `Mathlib.Topology.Hom.Open` `Mathlib.Topology.Homeomorph.Lemmas` `Mathlib.Topology.IndicatorConstPointwise` `Mathlib.Topology.Inseparable` `Mathlib.Topology.Instances.Discrete` `Mathlib.Topology.Instances.ENat` `Mathlib.Topology.Instances.Int` `Mathlib.Topology.Instances.Nat` `Mathlib.Topology.Instances.PNat` `Mathlib.Topology.Instances.Sign` `Mathlib.Topology.Irreducible` `Mathlib.Topology.List` `Mathlib.Topology.LocallyClosed` `Mathlib.Topology.LocallyFinite` `Mathlib.Topology.Maps.Proper.Basic` `Mathlib.Topology.Maps.Proper.UniversallyClosed` `Mathlib.Topology.MetricSpace.Antilipschitz` `Mathlib.Topology.MetricSpace.Basic` `Mathlib.Topology.MetricSpace.Bounded` `Mathlib.Topology.MetricSpace.Cauchy` `Mathlib.Topology.MetricSpace.Congruence` `Mathlib.Topology.MetricSpace.Defs` `Mathlib.Topology.MetricSpace.Equicontinuity` `Mathlib.Topology.MetricSpace.Gluing` `Mathlib.Topology.MetricSpace.Infsep` `Mathlib.Topology.MetricSpace.Isometry` `Mathlib.Topology.MetricSpace.MetricSeparated` `Mathlib.Topology.MetricSpace.ProperSpace.Lemmas` `Mathlib.Topology.MetricSpace.ProperSpace.Real` `Mathlib.Topology.MetricSpace.ProperSpace` `Mathlib.Topology.MetricSpace.Pseudo.Basic` `Mathlib.Topology.MetricSpace.Pseudo.Constructions` `Mathlib.Topology.MetricSpace.Pseudo.Defs` `Mathlib.Topology.MetricSpace.Pseudo.Lemmas` `Mathlib.Topology.MetricSpace.Pseudo.Pi` `Mathlib.Topology.MetricSpace.Pseudo.Real` `Mathlib.Topology.MetricSpace.Sequences` `Mathlib.Topology.MetricSpace.Similarity` `Mathlib.Topology.MetricSpace.Ultra.Basic` `Mathlib.Topology.MetricSpace.Ultra.Pi` `Mathlib.Topology.MetricSpace.Ultra.TotallySeparated` `Mathlib.Topology.Metrizable.Basic` `Mathlib.Topology.Metrizable.CompletelyMetrizable` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Topology.Metrizable.Real` `Mathlib.Topology.Metrizable.Uniformity` `Mathlib.Topology.OmegaCompletePartialOrder` `Mathlib.Topology.Order.Basic` `Mathlib.Topology.Order.Bornology` `Mathlib.Topology.Order.Category.AlexDisc` `Mathlib.Topology.Order.Compact` `Mathlib.Topology.Order.DenselyOrdered` `Mathlib.Topology.Order.ExtendFrom` `Mathlib.Topology.Order.ExtrClosure` `Mathlib.Topology.Order.Filter` `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.Real` `Mathlib.Topology.Order.Rolle` `Mathlib.Topology.Order.ScottTopology` `Mathlib.Topology.Order.T5` `Mathlib.Topology.Order.UpperLowerSetTopology` `Mathlib.Topology.Perfect` `Mathlib.Topology.Piecewise` `Mathlib.Topology.PreorderRestrict` `Mathlib.Topology.RestrictGen` `Mathlib.Topology.SeparatedMap` `Mathlib.Topology.Separation.Basic` `Mathlib.Topology.Separation.CountableSeparatingOn` `Mathlib.Topology.Separation.GDelta` `Mathlib.Topology.Separation.Hausdorff` `Mathlib.Topology.Separation.Profinite` `Mathlib.Topology.Separation.Regular` `Mathlib.Topology.Sequences` `Mathlib.Topology.ShrinkingLemma` `Mathlib.Topology.Specialization` `Mathlib.Topology.Spectral.Hom` `Mathlib.Topology.StoneCech` `Mathlib.Topology.Ultrafilter` `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.Equicontinuity` `Mathlib.Topology.UniformSpace.Equiv` `Mathlib.Topology.UniformSpace.HeineCantor` `Mathlib.Topology.UniformSpace.OfCompactT2` `Mathlib.Topology.UniformSpace.Pi` `Mathlib.Topology.UniformSpace.Real` `Mathlib.Topology.UniformSpace.Separation` `Mathlib.Topology.UniformSpace.Ultra.Basic` `Mathlib.Topology.UniformSpace.Ultra.Constructions` `Mathlib.Topology.UniformSpace.UniformConvergenceTopology` `Mathlib.Topology.UniformSpace.UniformConvergence` `Mathlib.Topology.UniformSpace.UniformEmbedding`	-3
956 files `Mathlib.Algebra.Algebra.ZMod` `Mathlib.Algebra.Azumaya.Basic` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.Azumaya.Matrix` `Mathlib.Algebra.Category.BialgebraCat.Basic` `Mathlib.Algebra.Category.BialgebraCat.Monoidal` `Mathlib.Algebra.Category.CoalgebraCat.Basic` `Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgebraCat.Monoidal` `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.Category.Grp.Adjunctions` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.IsFinite` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Category.HopfAlgebraCat.Basic` `Mathlib.Algebra.Category.HopfAlgebraCat.Monoidal` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Algebra.Category.ModuleCat.Kernels` `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.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.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Central.TensorProduct` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Algebra.CharP.Quotient` `Mathlib.Algebra.CharP.Two` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.Exact` `Mathlib.Algebra.Field.NegOnePow` `Mathlib.Algebra.Field.Periodic` `Mathlib.Algebra.Field.ZMod` `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.Algebra.Homology.BifunctorAssociator` `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Algebra.Homology.Bifunctor` `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.ExactSequences` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Algebra.Homology.Embedding.CochainComplex` `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.LocalCohomology` `Mathlib.Algebra.Homology.Monoidal` `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `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.CartanSubalgebra` `Mathlib.Algebra.Lie.Character` `Mathlib.Algebra.Lie.Derivation.AdjointAction` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.Semisimple.Basic` `Mathlib.Algebra.Lie.Semisimple.Defs` `Mathlib.Algebra.Lie.Solvable` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.Algebra.Module.Lattice` `Mathlib.Algebra.Module.LocalizedModule.Exact` `Mathlib.Algebra.Module.LocalizedModule.Submodule` `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.SnakeLemma` `Mathlib.Algebra.Module.SpanRank` `Mathlib.Algebra.Order.Archimedean.IndicatorCard` `Mathlib.Algebra.Order.Floor.Prime` `Mathlib.Algebra.Order.ToIntervalMod` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Quaternion` `Mathlib.Algebra.Ring.NegOnePow` `Mathlib.Algebra.Ring.Periodic` `Mathlib.Algebra.Star.CHSH` `Mathlib.Algebra.Symmetrized` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.Exposed` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Hofer` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.Meromorphic.Divisor.Basic` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Field.Instances` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.ProperSpace` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.SeparationQuotient` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.InfiniteSum` `Mathlib.Analysis.Normed.Ring.Lemmas` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Analysis.Oscillation` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.Choose` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Analysis.Subadditive` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.CategoryTheory.Abelian.FreydMitchell` `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.Injective.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Dimension` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Action` `Mathlib.CategoryTheory.Galois.Action` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.CategoryTheory.Galois.Full` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.CategoryTheory.Galois.Prorepresentability` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.CategoryTheory.Localization.Triangulated` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.CategoryTheory.Sites.Spaces` `Mathlib.CategoryTheory.SmallObject.Basic` `Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument` `Mathlib.CategoryTheory.Triangulated.Adjunction` `Mathlib.CategoryTheory.Triangulated.Functor` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.CategoryTheory.Triangulated.Opposite.Functor` `Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.CategoryTheory.Triangulated.TStructure.Basic` `Mathlib.CategoryTheory.Triangulated.TriangleShift` `Mathlib.CategoryTheory.Triangulated.Triangulated` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.Combinatorics.Additive.ApproximateSubgroup` `Mathlib.Combinatorics.Additive.RuzsaCovering` `Mathlib.Combinatorics.Additive.VerySmallDoubling` `Mathlib.Combinatorics.SimpleGraph.AdjMatrix` `Mathlib.Combinatorics.SimpleGraph.Bipartite` `Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents` `Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph` `Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting` `Mathlib.Combinatorics.SimpleGraph.DegreeSum` `Mathlib.Combinatorics.SimpleGraph.Matching` `Mathlib.Combinatorics.SimpleGraph.StronglyRegular` `Mathlib.Combinatorics.SimpleGraph.UniversalVerts` `Mathlib.Condensed.AB` `Mathlib.Condensed.Basic` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Condensed.Discrete.Characterization` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Condensed.Discrete.Module` `Mathlib.Condensed.Epi` `Mathlib.Condensed.Equivalence` `Mathlib.Condensed.Explicit` `Mathlib.Condensed.Functors` `Mathlib.Condensed.Light.AB` `Mathlib.Condensed.Light.Basic` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Condensed.Light.Epi` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Light.Functors` `Mathlib.Condensed.Light.Limits` `Mathlib.Condensed.Light.Module` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.Limits` `Mathlib.Condensed.Module` `Mathlib.Condensed.Solid` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Condensed.TopComparison` `Mathlib.Data.Complex.Cardinality` `Mathlib.Data.Complex.Exponential` `Mathlib.Data.Complex.FiniteDimensional` `Mathlib.Data.Complex.Norm` `Mathlib.Data.Complex.Order` `Mathlib.Data.Complex.Trigonometric` `Mathlib.Data.Nat.Periodic` `Mathlib.Data.Nat.Totient` `Mathlib.Data.Real.Cardinality` `Mathlib.Data.Real.CompleteField` `Mathlib.Data.Real.Hyperreal` `Mathlib.Data.Real.IsNonarchimedean` `Mathlib.Data.Real.Sqrt` `Mathlib.Data.Real.StarOrdered` `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.NormedSpace` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Dynamics.Ergodic.Action.Regular` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.Dynamics.Flow` `Mathlib.Dynamics.OmegaLimit` `Mathlib.FieldTheory.Finiteness` `Mathlib.FieldTheory.Tower` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Manifold.ChartedSpace` `Mathlib.Geometry.Manifold.LocalInvariantProperties` `Mathlib.Geometry.Manifold.Sheaf.Basic` `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.Commensurable` `Mathlib.GroupTheory.Commutator.Finite` `Mathlib.GroupTheory.CommutingProbability` `Mathlib.GroupTheory.Complement` `Mathlib.GroupTheory.CosetCover` `Mathlib.GroupTheory.Coxeter.Inversion` `Mathlib.GroupTheory.Coxeter.Length` `Mathlib.GroupTheory.Exponent` `Mathlib.GroupTheory.Finiteness` `Mathlib.GroupTheory.FreeAbelianGroupFinsupp` `Mathlib.GroupTheory.FreeAbelianGroup` `Mathlib.GroupTheory.FreeGroup.NielsenSchreier` `Mathlib.GroupTheory.GroupAction.Blocks` `Mathlib.GroupTheory.GroupAction.Iwasawa` `Mathlib.GroupTheory.GroupAction.Period` `Mathlib.GroupTheory.GroupAction.Primitive` `Mathlib.GroupTheory.GroupExtension.Basic` `Mathlib.GroupTheory.GroupExtension.Defs` `Mathlib.GroupTheory.HNNExtension` `Mathlib.GroupTheory.IndexNormal` `Mathlib.GroupTheory.Index` `Mathlib.GroupTheory.NoncommPiCoprod` `Mathlib.GroupTheory.OrderOfElement` `Mathlib.GroupTheory.Perm.Finite` `Mathlib.GroupTheory.PushoutI` `Mathlib.GroupTheory.QuotientGroup.Finite` `Mathlib.GroupTheory.SemidirectProduct` `Mathlib.GroupTheory.Solvable` `Mathlib.GroupTheory.SpecificGroups.Cyclic` `Mathlib.GroupTheory.SpecificGroups.Dihedral` `Mathlib.GroupTheory.SpecificGroups.KleinFour` `Mathlib.GroupTheory.SpecificGroups.Quaternion` `Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.LinearAlgebra.Basis.Exact` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `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.Eigenspace.Basic` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.LinearAlgebra.FiniteDimensional.Basic` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FiniteDimensional.Lemmas` `Mathlib.LinearAlgebra.FiniteSpan` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.LinearAlgebra.FreeModule.Int` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.Goursat` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.LinearAlgebra.Isomorphisms` `Mathlib.LinearAlgebra.LinearDisjoint` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.LinearAlgebra.Projection` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.LinearAlgebra.Quotient.Basic` `Mathlib.LinearAlgebra.Quotient.Pi` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.LinearAlgebra.TensorProduct.Graded.External` `Mathlib.LinearAlgebra.TensorProduct.Graded.Internal` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Decomposition.Jordan` `Mathlib.MeasureTheory.Decomposition.SignedHahn` `Mathlib.MeasureTheory.Decomposition.UnsignedHahn` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.AEEqOfLIntegral` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.MeasureTheory.Group.Action` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.MeasureTheory.Group.LIntegral` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.MeasureTheory.Group.Measure` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.MeasureTheory.Group.Prod` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.MeasureTheory.Integral.Lebesgue` `Mathlib.MeasureTheory.MeasurableSpace.NCard` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.MeasureTheory.Measure.Map` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Measure.Prod` `Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Measure.RegularityCompacts` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.MeasureTheory.Measure.Tight` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.MeasureTheory.Measure.WithDensity` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.OuterMeasure.OfAddContent` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.MeasureTheory.Topology` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.ModelTheory.DirectLimit` `Mathlib.ModelTheory.FinitelyGenerated` `Mathlib.ModelTheory.Fraisse` `Mathlib.ModelTheory.PartialEquiv` `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.DirichletCharacter.Basic` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.NumberTheory.FLT.Four` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.LegendreSymbol.ZModChar` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MulChar.Basic` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.NumberTheory.PythagoreanTriples` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Order.Filter.Cocardinal` `Mathlib.Order.Filter.ENNReal` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Independence.Basic` `Mathlib.Probability.Independence.Kernel` `Mathlib.Probability.Kernel.Basic` `Mathlib.Probability.Kernel.Composition.CompMap` `Mathlib.Probability.Kernel.Composition.CompNotation` `Mathlib.Probability.Kernel.Composition.CompProd` `Mathlib.Probability.Kernel.Composition.Comp` `Mathlib.Probability.Kernel.Composition.MapComap` `Mathlib.Probability.Kernel.Composition.ParallelComp` `Mathlib.Probability.Kernel.Composition.Prod` `Mathlib.Probability.Kernel.Defs` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj` `Mathlib.Probability.Kernel.MeasurableLIntegral` `Mathlib.Probability.Kernel.Proper` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.Probability.UniformOn` `Mathlib.RepresentationTheory.Maschke` `Mathlib.RingTheory.Adjoin.Dimension` `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.TensorProduct` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.FiniteLength` `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.Subalgebra` `Mathlib.RingTheory.Fintype` `Mathlib.RingTheory.Flat.Basic` `Mathlib.RingTheory.Flat.CategoryTheory` `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.FractionalIdeal.Basic` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.FreeRing` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.HopfAlgebra.Basic` `Mathlib.RingTheory.HopfAlgebra.TensorProduct` `Mathlib.RingTheory.Ideal.AssociatedPrime` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.Ideal.MinimalPrime.Basic` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.Ideal.Over` `Mathlib.RingTheory.Ideal.Quotient.Basic` `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.Int.Basic` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.Jacobson.Radical` `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.LocalSubring` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.RingTheory.Morita.Basic` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.RingTheory.MvPowerSeries.Evaluation` `Mathlib.RingTheory.MvPowerSeries.LinearTopology` `Mathlib.RingTheory.MvPowerSeries.PiTopology` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Nilpotent.Lemmas` `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.OrzechProperty` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.RingTheory.SimpleModule.Rank` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.RingTheory.Spectrum.Maximal.Localization` `Mathlib.RingTheory.Spectrum.Prime.Basic` `Mathlib.RingTheory.Spectrum.Prime.RingHom` `Mathlib.RingTheory.Support` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.TensorProduct.Nontrivial` `Mathlib.RingTheory.TensorProduct.Quotient` `Mathlib.RingTheory.Valuation.Archimedean` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.RingTheory.ZMod` `Mathlib.SetTheory.Cardinal.Finsupp` `Mathlib.SetTheory.Nimber.Field` `Mathlib.SetTheory.Ordinal.Topology` `Mathlib.SetTheory.Surreal.Dyadic` `Mathlib.SetTheory.Surreal.Multiplication` `Mathlib.Tactic.NormNum.RealSqrt` `Mathlib.Topology.Algebra.Affine` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits` `Mathlib.Topology.Algebra.ClopenNhdofOne` `Mathlib.Topology.Algebra.ClosedSubgroup` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Topology.Algebra.ContinuousMonoidHom` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.Topology.Algebra.Field` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Group.Basic` `Mathlib.Topology.Algebra.Group.CompactOpen` `Mathlib.Topology.Algebra.Group.Compact` `Mathlib.Topology.Algebra.Group.GroupTopology` `Mathlib.Topology.Algebra.Group.OpenMapping` `Mathlib.Topology.Algebra.Group.Pointwise` `Mathlib.Topology.Algebra.Group.Quotient` `Mathlib.Topology.Algebra.Group.SubmonoidClosure` `Mathlib.Topology.Algebra.Group.TopologicalAbelianization` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.Topology.Algebra.IsOpenUnits` `Mathlib.Topology.Algebra.LinearTopology` `Mathlib.Topology.Algebra.Localization` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.Topology.Algebra.Module.CharacterSpace` `Mathlib.Topology.Algebra.Module.Compact` `Mathlib.Topology.Algebra.Module.Equiv` `Mathlib.Topology.Algebra.Module.LinearMapPiProd` `Mathlib.Topology.Algebra.Module.LinearMap` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Module.WeakBilin` `Mathlib.Topology.Algebra.Module.WeakDual` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.Topology.Algebra.Nonarchimedean.Basic` `Mathlib.Topology.Algebra.Nonarchimedean.Completion` `Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected` `Mathlib.Topology.Algebra.OpenSubgroup` `Mathlib.Topology.Algebra.Order.Field` `Mathlib.Topology.Algebra.Order.Floor` `Mathlib.Topology.Algebra.Order.Group` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.RestrictedProduct` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.Topology.Algebra.Ring.Ideal` `Mathlib.Topology.Algebra.Ring.Real` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.Topology.Algebra.SeparationQuotient.Hom` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Algebra.UniformConvergence` `Mathlib.Topology.Algebra.UniformField` `Mathlib.Topology.Algebra.UniformFilterBasis` `Mathlib.Topology.Algebra.UniformGroup.Basic` `Mathlib.Topology.Algebra.UniformGroup.Defs` `Mathlib.Topology.Algebra.UniformMulAction` `Mathlib.Topology.Algebra.UniformRing` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.Topology.Baire.CompleteMetrizable` `Mathlib.Topology.Baire.LocallyCompactRegular` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.CWComplex.Classical.Basic` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.Category.CompHaus.Frm` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.Topology.Category.Compactum` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Topology.Category.Locale` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Topology.Category.Profinite.Extend` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.Topology.Category.TopCat.OpenNhds` `Mathlib.Topology.Category.TopCat.Opens` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Topology.ClopenBox` `Mathlib.Topology.Compactification.OnePointEquiv` `Mathlib.Topology.Compactification.OnePoint` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Connected.LocPathConnected` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Topology.Constructible` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.Topology.ContinuousMap.Periodic` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Topology.ContinuousMap.T0Sierpinski` `Mathlib.Topology.Covering` `Mathlib.Topology.DiscreteQuotient` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.EMetricSpace.Paracompact` `Mathlib.Topology.FiberBundle.Basic` `Mathlib.Topology.FiberBundle.Constructions` `Mathlib.Topology.FiberBundle.Trivialization` `Mathlib.Topology.FiberPartition` `Mathlib.Topology.Germ` `Mathlib.Topology.Gluing` `Mathlib.Topology.Homotopy.Basic` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Lifting` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Instances.AddCircle` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.EReal.Lemmas` `Mathlib.Topology.Instances.NNReal.Lemmas` `Mathlib.Topology.Instances.Rat` `Mathlib.Topology.Instances.Real.Lemmas` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Topology.IsLocalHomeomorph` `Mathlib.Topology.JacobsonSpace` `Mathlib.Topology.KrullDimension` `Mathlib.Topology.LocalAtTarget` `Mathlib.Topology.LocallyConstant.Algebra` `Mathlib.Topology.LocallyConstant.Basic` `Mathlib.Topology.Maps.Proper.CompactlyGenerated` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.Topology.MetricSpace.Bilipschitz` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.DilationEquiv` `Mathlib.Topology.MetricSpace.Dilation` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Topology.MetricSpace.IsometricSMul` `Mathlib.Topology.MetricSpace.Lipschitz` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.Topology.MetricSpace.ShrinkingLemma` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Topology.NoetherianSpace` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.PartialHomeomorph` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Path` `Mathlib.Topology.QuasiSeparated` `Mathlib.Topology.Semicontinuous` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.DisjointCover` `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.CommRingCat` `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.Sober` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.Topology.UnitInterval` `Mathlib.Topology.UrysohnsLemma`	-2
668 files `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.Algebra.DirectSum.LinearMap` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `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.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.Group` `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Complex.Tietze` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Analysis.Convex.Cone.Pointed` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Analysis.Convex.Continuous` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.Measure` `Mathlib.Analysis.Convolution` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Analysis.InnerProductSpace.Projection` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.Analysis.LocallyConvex.WeakOperatorTopology` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.Analysis.Normed.Affine.Convex` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.NormedSpace.HahnBanach.Extension` `Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Configuration` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Computability.Ackermann` `Mathlib.Computability.Halting` `Mathlib.Computability.PartrecCode` `Mathlib.Computability.Partrec` `Mathlib.Computability.Primrec` `Mathlib.Computability.Reduce` `Mathlib.Computability.TMConfig` `Mathlib.Computability.TMToPartrec` `Mathlib.Data.DFinsupp.Encodable` `Mathlib.Data.Finsupp.Encodable` `Mathlib.Data.Matrix.Rank` `Mathlib.Data.PFunctor.Multivariate.Basic` `Mathlib.Data.PFunctor.Multivariate.M` `Mathlib.Data.PFunctor.Multivariate.W` `Mathlib.Data.PFunctor.Univariate.Basic` `Mathlib.Data.PFunctor.Univariate.M` `Mathlib.Data.QPF.Multivariate.Basic` `Mathlib.Data.QPF.Multivariate.Constructions.Cofix` `Mathlib.Data.QPF.Multivariate.Constructions.Comp` `Mathlib.Data.QPF.Multivariate.Constructions.Const` `Mathlib.Data.QPF.Multivariate.Constructions.Fix` `Mathlib.Data.QPF.Multivariate.Constructions.Prj` `Mathlib.Data.QPF.Multivariate.Constructions.Quot` `Mathlib.Data.QPF.Multivariate.Constructions.Sigma` `Mathlib.Data.QPF.Univariate.Basic` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Data.W.Basic` `Mathlib.Data.W.Cardinal` `Mathlib.Data.W.Constructions` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Extension` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Fixed` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.IntermediateField.Adjoin.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.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.Minpoly.IsConjRoot` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure` `Mathlib.FieldTheory.NormalizedTrace` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.Exponent` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.Relrank` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.Geometry.Euclidean.Sphere.Power` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.Geometry.Manifold.ContMDiff.Constructions` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.Geometry.Manifold.IsManifold.ExtChartAt` `Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Geometry.Manifold.VectorField.LieBracket` `Mathlib.Geometry.Manifold.VectorField.Pullback` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.InformationTheory.KullbackLeibler.Basic` `Mathlib.InformationTheory.KullbackLeibler.KLFun` `Mathlib.LinearAlgebra.BilinearForm.DualLattice` `Mathlib.LinearAlgebra.BilinearForm.Orthogonal` `Mathlib.LinearAlgebra.BilinearForm.Properties` `Mathlib.LinearAlgebra.BilinearForm.TensorProduct` `Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange` `Mathlib.LinearAlgebra.Coevaluation` `Mathlib.LinearAlgebra.Contraction` `Mathlib.LinearAlgebra.Countable` `Mathlib.LinearAlgebra.Dimension.ErdosKaplansky` `Mathlib.LinearAlgebra.Dual.Lemmas` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.Matrix.BilinearForm` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.LinearAlgebra.Matrix.Hermitian` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.LinearAlgebra.PID` `Mathlib.LinearAlgebra.PerfectPairing.Basic` `Mathlib.LinearAlgebra.PerfectPairing.Restrict` `Mathlib.LinearAlgebra.QuadraticForm.Dual` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Defs` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.Irreducible` `Mathlib.LinearAlgebra.RootSystem.OfBilinear` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.Trace` `Mathlib.Logic.Encodable.Pi` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.MeasureTheory.Constructions.Pi` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.MeasureTheory.Function.FactorsThrough` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.MeasureTheory.Group.ModularCharacter` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.IntegrationByParts` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.MeasureTheory.Integral.Marginal` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Integral.Periodic` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.MeasureTheory.Integral.SetIntegral` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.FiniteMeasureExt` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.MeasureTheory.Measure.Lebesgue.Complex` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.NumberTheory.LSeries.Injectivity` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.NumberTheory.LSeries.SumCoeff` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.CDF` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.Density` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Integration` `Mathlib.Probability.Kernel.CompProdEqIff` `Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous` `Mathlib.Probability.Kernel.Composition.IntegralCompProd` `Mathlib.Probability.Kernel.Composition.Lemmas` `Mathlib.Probability.Kernel.Composition.MeasureCompProd` `Mathlib.Probability.Kernel.Composition.MeasureComp` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Probability.Kernel.IonescuTulcea.Traj` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Probability.Kernel.Posterior` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.Probability.Kernel.SetIntegral` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Probability.Martingale.Basic` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Probability.Martingale.Centering` `Mathlib.Probability.Martingale.Convergence` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.Probability.Moments.Basic` `Mathlib.Probability.Moments.ComplexMGF` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Moments.SubGaussian` `Mathlib.Probability.Moments.Tilted` `Mathlib.Probability.Notation` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.StrongLaw` `Mathlib.Probability.Variance` `Mathlib.RepresentationTheory.Basic` `Mathlib.RepresentationTheory.Character` `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.Rep` `Mathlib.RepresentationTheory.Submodule` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality` `Mathlib.RingTheory.Complex` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.Invariant` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Norm.Basic` `Mathlib.RingTheory.NormTrace` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Defs` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Valuation.Minpoly` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.RingTheory.WittVector.Compare` `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.SetTheory.Cardinal.Subfield` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.CWComplex.Abstract.Basic` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.MetricSpace.HausdorffDimension`	2
`Mathlib.Logic.Equiv.Multiset` (new file)	469
`Mathlib.Logic.Equiv.Finset` (new file)	483

Declarations diff

+ Finset.encodable
+ instance _root_.Multiset.countable [Countable α] : Countable (Multiset α)
- instance _root_.Finset.encodable [Encodable α] : Encodable (Finset α)
- instance _root_.Multiset.countable {α : Type*} [Countable α] : Countable (Multiset α)

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).

Vierkantor · 2025-03-19T11:03:23Z

Mathlib/Logic/Equiv/List.lean

+instance _root_.Finset.countable [Countable α] : Countable (Finset α) :=
+  Finset.val_injective.countable


Oh I see, this is what makes Data.Set.Countable still work!

Vierkantor

Nice work!

bors d+

mathlib-bors · 2025-03-19T11:04:21Z

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser · 2025-03-19T12:24:39Z

bors merge

The motivation here is to delay the import of sorting.

mathlib-bors · 2025-03-19T13:11:47Z

Pull request successfully merged into master.

Build succeeded:

The motivation here is to delay the import of sorting.

refactor(Logic/Equiv/List): split

a11622e

eric-wieser requested a review from Vierkantor March 19, 2025 10:46

fix namespace

a351945

eric-wieser mentioned this pull request Mar 19, 2025

[Merged by Bors] - feat(Data/Finset/Sum): supremum over a disjoint union #22983

Closed

Vierkantor reviewed Mar 19, 2025

View reviewed changes

Vierkantor approved these changes Mar 19, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 19, 2025

eric-wieser added 2 commits March 19, 2025 11:31

fix imports

4f1da92

tweak imports

96ea62b

ghost added the ready-to-merge This PR has been sent to bors. label Mar 19, 2025

mathlib-bors bot pushed a commit that referenced this pull request Mar 19, 2025

refactor(Logic/Equiv/List): split (#23092)

4aa8b04

The motivation here is to delay the import of sorting.

mathlib-bors bot changed the title ~~refactor(Logic/Equiv/List): split~~ [Merged by Bors] - refactor(Logic/Equiv/List): split Mar 19, 2025

mathlib-bors bot closed this Mar 19, 2025

mathlib-bors bot deleted the eric-wieser/split-logic-equiv-list branch March 19, 2025 13:11

tukamilano pushed a commit that referenced this pull request Mar 20, 2025

refactor(Logic/Equiv/List): split (#23092)

7549acf

The motivation here is to delay the import of sorting.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(Logic/Equiv/List): split#23092

[Merged by Bors] - refactor(Logic/Equiv/List): split#23092
eric-wieser wants to merge 4 commits intomasterfrom
eric-wieser/split-logic-equiv-list

eric-wieser commented Mar 19, 2025

Uh oh!

github-actions bot commented Mar 19, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Vierkantor Mar 19, 2025

Uh oh!

Vierkantor left a comment

Uh oh!

mathlib-bors bot commented Mar 19, 2025

Uh oh!

eric-wieser commented Mar 19, 2025

Uh oh!

mathlib-bors bot commented Mar 19, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		instance _root_.Finset.countable [Countable α] : Countable (Finset α) :=
		Finset.val_injective.countable

Conversation

eric-wieser commented Mar 19, 2025

Uh oh!

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

Uh oh!

PR summary 96ea62b47a

Import changes for modified files

Declarations diff

Uh oh!

Vierkantor Mar 19, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 19, 2025

Uh oh!

eric-wieser commented Mar 19, 2025

Uh oh!

mathlib-bors bot commented Mar 19, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions bot commented Mar 19, 2025 •

edited

Loading