[Merged by Bors] - chore(Data/Fintype): split `Fintype/Card.lean` by Vierkantor · Pull Request #21840 · leanprover-community/mathlib4

Vierkantor · 2025-02-13T18:18:12Z

This PR splits Data.Fintype.Card based on dependencies:

Data.Fintype.Card contains the definition of Fintype.card and basic results
Data.Fintype.EquivFin contains the equivalences between fintypes, finiteness and Fin
Data.Fintype.Pigeonhole contains a few pigeonhole principles
Data.Fintype.Group gets a few extra results on Additive/Multiplicative

depends on: [Merged by Bors] - chore(Data/Fintype): split Data/Fintype/Basic.lean #21831

github-actions · 2025-02-14T09:39:02Z

PR summary 811f6c1679

Import changes exceeding 2%

%	File
+3.87%	`Mathlib.Algebra.Group.TypeTags.Fintype`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Fintype.Card	479	424	-55 (-11.48%)
Mathlib.Data.Finite.Set	480	459	-21 (-4.38%)
Mathlib.Algebra.CharZero.Infinite	481	460	-21 (-4.37%)
Mathlib.Data.Set.Finite.Range	482	461	-21 (-4.36%)
Mathlib.Data.Fintype.Shrink	484	463	-21 (-4.34%)
Mathlib.CategoryTheory.FinCategory.AsType	510	489	-21 (-4.12%)
Mathlib.CategoryTheory.Countable	534	513	-21 (-3.93%)
Mathlib.Algebra.Group.TypeTags.Fintype	413	429	+16 (+3.87%)
Mathlib.CategoryTheory.EffectiveEpi.Preserves	548	527	-21 (-3.83%)
Mathlib.Logic.Denumerable	505	486	-19 (-3.76%)
Mathlib.Data.Finset.Sort	504	486	-18 (-3.57%)
Mathlib.Logic.Equiv.List	523	506	-17 (-3.25%)
Mathlib.Data.Fintype.Perm	492	479	-13 (-2.64%)
Mathlib.Data.ZMod.Defs	508	496	-12 (-2.36%)
Mathlib.Algebra.Group.Submonoid.Membership	510	499	-11 (-2.16%)
Mathlib.Data.FinEnum	482	478	-4 (-0.83%)
Mathlib.Data.Set.Finite.Basic	480	479	-1 (-0.21%)
Mathlib.Data.Fintype.Option	481	480	-1 (-0.21%)
Mathlib.Data.Fintype.Prod	481	480	-1 (-0.21%)
Mathlib.Data.Fintype.Sum	485	484	-1 (-0.21%)
Mathlib.Data.Finite.Vector	502	501	-1 (-0.20%)
Mathlib.Data.Finite.Sigma	503	502	-1 (-0.20%)
Mathlib.Data.Fintype.Powerset	506	505	-1 (-0.20%)

Import changes for all files

Files	Import difference
`Mathlib.Data.Fintype.Card`	-55
`Mathlib.Combinatorics.SetFamily.Intersecting`	-50
`Mathlib.Data.Fintype.Parity`	-44
`Mathlib.GroupTheory.Coset.Basic`	-28
4 files `Mathlib.Algebra.Field.Action.ConjAct` `Mathlib.Algebra.GroupWithZero.Action.ConjAct` `Mathlib.Algebra.Ring.Action.ConjAct` `Mathlib.GroupTheory.GroupAction.ConjAct`	-27
`Mathlib.Data.Finset.Density`	-24
8 files `Mathlib.Algebra.CharZero.Infinite` `Mathlib.CategoryTheory.Countable` `Mathlib.CategoryTheory.EffectiveEpi.Preserves` `Mathlib.CategoryTheory.FinCategory.AsType` `Mathlib.Data.Finite.Set` `Mathlib.Data.Fintype.Shrink` `Mathlib.Data.MLList.BestFirst` `Mathlib.Data.Set.Finite.Range`	-21
`Mathlib.Logic.Denumerable`	-19
`Mathlib.Data.Finset.Sort` `Mathlib.Data.Fintype.Sort`	-18
18 files `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.W.Basic` `Mathlib.Data.W.Constructions` `Mathlib.Logic.Equiv.Array` `Mathlib.Logic.Equiv.List`	-17
`Mathlib.Data.Fintype.Perm`	-13
`Mathlib.Data.Fin.Parity` `Mathlib.Data.ZMod.Defs`	-12
6 files `Mathlib.Algebra.Group.Submonoid.Membership` `Mathlib.Algebra.GroupWithZero.NonZeroDivisors` `Mathlib.Algebra.Ring.NonZeroDivisors` `Mathlib.GroupTheory.Coprod.Basic` `Mathlib.RingTheory.NonUnitalSubsemiring.Basic` `Mathlib.RingTheory.OreLocalization.Ring`	-11
`Mathlib.Data.BitVec` `Mathlib.Data.UInt`	-10
`Mathlib.Data.Rat.Denumerable`	-9
`Mathlib.Algebra.Quandle`	-8
5 files `Mathlib.Computability.Halting` `Mathlib.Computability.PartrecCode` `Mathlib.Computability.Partrec` `Mathlib.Computability.Primrec` `Mathlib.Computability.Reduce`	-7
`Mathlib.Computability.Ackermann` `Mathlib.NumberTheory.FrobeniusNumber`	-6
`Mathlib.Data.FinEnum`	-4
`Mathlib.Data.FinEnum.Option`	-3
293 files `Mathlib.Algebra.Group.FiniteSupport` `Mathlib.Algebra.Homology.ShortComplex.Homology` `Mathlib.Algebra.Homology.ShortComplex.Limits` `Mathlib.Algebra.Homology.ShortComplex.PreservesHomology` `Mathlib.Algebra.Homology.ShortComplex.QuasiIso` `Mathlib.Algebra.Homology.ShortComplex.Retract` `Mathlib.Algebra.Homology.ShortComplex.RightHomology` `Mathlib.Algebra.Order.Antidiag.Prod` `Mathlib.Algebra.Order.Disjointed` `Mathlib.Algebra.Order.Interval.Finset` `Mathlib.Algebra.Order.Interval.Multiset` `Mathlib.Algebra.Order.PartialSups` `Mathlib.AlgebraicTopology.ModelCategory.Basic` `Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells` `Mathlib.CategoryTheory.Adjunction.Lifting.Left` `Mathlib.CategoryTheory.Adjunction.Lifting.Right` `Mathlib.CategoryTheory.ChosenFiniteProducts.Cat` `Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory` `Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice` `Mathlib.CategoryTheory.ChosenFiniteProducts` `Mathlib.CategoryTheory.Closed.Cartesian` `Mathlib.CategoryTheory.Closed.Enrichment` `Mathlib.CategoryTheory.Closed.FunctorCategory.Basic` `Mathlib.CategoryTheory.Closed.FunctorCategory.Complete` `Mathlib.CategoryTheory.Closed.FunctorToTypes` `Mathlib.CategoryTheory.Closed.Functor` `Mathlib.CategoryTheory.Closed.Ideal` `Mathlib.CategoryTheory.Closed.Types` `Mathlib.CategoryTheory.Closed.Zero` `Mathlib.CategoryTheory.Comma.Final` `Mathlib.CategoryTheory.Comma.Presheaf.Colimit` `Mathlib.CategoryTheory.ConcreteCategory.EpiMono` `Mathlib.CategoryTheory.Dialectica.Basic` `Mathlib.CategoryTheory.Enriched.Basic` `Mathlib.CategoryTheory.Enriched.FunctorCategory` `Mathlib.CategoryTheory.Enriched.HomCongr` `Mathlib.CategoryTheory.Enriched.Opposite` `Mathlib.CategoryTheory.Enriched.Ordinary.Basic` `Mathlib.CategoryTheory.Filtered.Basic` `Mathlib.CategoryTheory.Filtered.Connected` `Mathlib.CategoryTheory.Filtered.CostructuredArrow` `Mathlib.CategoryTheory.Filtered.Final` `Mathlib.CategoryTheory.Filtered.Flat` `Mathlib.CategoryTheory.Filtered.Grothendieck` `Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Filtered.Small` `Mathlib.CategoryTheory.FintypeCat` `Mathlib.CategoryTheory.Functor.Flat` `Mathlib.CategoryTheory.Functor.FunctorHom` `Mathlib.CategoryTheory.GlueData` `Mathlib.CategoryTheory.GradedObject.Braiding` `Mathlib.CategoryTheory.GradedObject.Monoidal` `Mathlib.CategoryTheory.GuitartExact.Basic` `Mathlib.CategoryTheory.GuitartExact.VerticalComposition` `Mathlib.CategoryTheory.LiftingProperties.Limits` `Mathlib.CategoryTheory.Limits.Comma` `Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic` `Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.EpiMono` `Mathlib.CategoryTheory.Limits.Constructions.Equalizers` `Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant` `Mathlib.CategoryTheory.Limits.Constructions.Filtered` `Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers` `Mathlib.CategoryTheory.Limits.Constructions.Over.Basic` `Mathlib.CategoryTheory.Limits.Constructions.Over.Products` `Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects` `Mathlib.CategoryTheory.Limits.EpiMono` `Mathlib.CategoryTheory.Limits.ExactFunctor` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct` `Mathlib.CategoryTheory.Limits.Filtered` `Mathlib.CategoryTheory.Limits.Final.ParallelPair` `Mathlib.CategoryTheory.Limits.Final` `Mathlib.CategoryTheory.Limits.FinallySmall` `Mathlib.CategoryTheory.Limits.FintypeCat` `Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono` `Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered` `Mathlib.CategoryTheory.Limits.FunctorCategory.Finite` `Mathlib.CategoryTheory.Limits.IndYoneda` `Mathlib.CategoryTheory.Limits.Indization.Category` `Mathlib.CategoryTheory.Limits.Indization.Equalizers` `Mathlib.CategoryTheory.Limits.Indization.FilteredColimits` `Mathlib.CategoryTheory.Limits.Indization.IndObject` `Mathlib.CategoryTheory.Limits.Indization.LocallySmall` `Mathlib.CategoryTheory.Limits.Indization.ParallelPair` `Mathlib.CategoryTheory.Limits.Indization.Products` `Mathlib.CategoryTheory.Limits.IsConnected` `Mathlib.CategoryTheory.Limits.Lattice` `Mathlib.CategoryTheory.Limits.MorphismProperty` `Mathlib.CategoryTheory.Limits.Opposites` `Mathlib.CategoryTheory.Limits.Over` `Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite` `Mathlib.CategoryTheory.Limits.Preserves.Filtered` `Mathlib.CategoryTheory.Limits.Preserves.Finite` `Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory` `Mathlib.CategoryTheory.Limits.Preserves.Opposites` `Mathlib.CategoryTheory.Limits.Preserves.Presheaf` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square` `Mathlib.CategoryTheory.Limits.Presheaf` `Mathlib.CategoryTheory.Limits.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory` `Mathlib.CategoryTheory.Limits.Shapes.Countable` `Mathlib.CategoryTheory.Limits.Shapes.Diagonal` `Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits` `Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts` `Mathlib.CategoryTheory.Limits.Shapes.KernelPair` `Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square` `Mathlib.CategoryTheory.Limits.Shapes.Reflexive` `Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct` `Mathlib.CategoryTheory.Limits.Sifted` `Mathlib.CategoryTheory.Limits.TypesFiltered` `Mathlib.CategoryTheory.Limits.VanKampen` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.CategoryTheory.Localization.Pi` `Mathlib.CategoryTheory.Monad.Coequalizer` `Mathlib.CategoryTheory.Monad.Comonadicity` `Mathlib.CategoryTheory.Monad.Equalizer` `Mathlib.CategoryTheory.Monad.Monadicity` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_` `Mathlib.CategoryTheory.Monoidal.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Grp_` `Mathlib.CategoryTheory.Monoidal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Types.Coyoneda` `Mathlib.CategoryTheory.MorphismProperty.LiftingProperty` `Mathlib.CategoryTheory.MorphismProperty.Limits` `Mathlib.CategoryTheory.MorphismProperty.OverAdjunction` `Mathlib.CategoryTheory.MorphismProperty.Representable` `Mathlib.CategoryTheory.MorphismProperty.RetractArgument` `Mathlib.CategoryTheory.Preadditive.Injective` `Mathlib.CategoryTheory.Preadditive.OfBiproducts` `Mathlib.CategoryTheory.Preadditive.Projective` `Mathlib.CategoryTheory.Sites.MorphismProperty` `Mathlib.CategoryTheory.Sites.Preserves` `Mathlib.CategoryTheory.SmallObject.Construction` `Mathlib.CategoryTheory.SmallObject.Iteration.Basic` `Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc` `Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone` `Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty` `Mathlib.CategoryTheory.Subobject.Comma` `Mathlib.CategoryTheory.Subpresheaf.Equalizer` `Mathlib.CategoryTheory.Subpresheaf.Image` `Mathlib.CategoryTheory.Subpresheaf.OfSection` `Mathlib.CategoryTheory.Subpresheaf.Subobject` `Mathlib.CategoryTheory.Triangulated.Basic` `Mathlib.Combinatorics.Digraph.Basic` `Mathlib.Combinatorics.Digraph.Orientation` `Mathlib.Combinatorics.Hall.Finite` `Mathlib.Combinatorics.SimpleGraph.Basic` `Mathlib.Combinatorics.SimpleGraph.Dart` `Mathlib.Combinatorics.SimpleGraph.LineGraph` `Mathlib.Combinatorics.SimpleGraph.Maps` `Mathlib.Combinatorics.SimpleGraph.Walk` `Mathlib.Combinatorics.Young.SemistandardTableau` `Mathlib.Combinatorics.Young.YoungDiagram` `Mathlib.Computability.ContextFreeGrammar` `Mathlib.Computability.Language` `Mathlib.Computability.RegularExpressions` `Mathlib.Computability.TuringMachine` `Mathlib.Data.Analysis.Filter` `Mathlib.Data.DFinsupp.Defs` `Mathlib.Data.DFinsupp.Encodable` `Mathlib.Data.DFinsupp.Ext` `Mathlib.Data.DFinsupp.FiniteInfinite` `Mathlib.Data.DFinsupp.NeLocus` `Mathlib.Data.DFinsupp.Notation` `Mathlib.Data.DFinsupp.Small` `Mathlib.Data.Fin.Tuple.Finset` `Mathlib.Data.Finite.Prod` `Mathlib.Data.Finite.Sigma` `Mathlib.Data.Finite.Sum` `Mathlib.Data.Finite.Vector` `Mathlib.Data.Finset.Functor` `Mathlib.Data.Finset.MulAntidiagonal` `Mathlib.Data.Finset.NAry` `Mathlib.Data.Finset.NatAntidiagonal` `Mathlib.Data.Finset.Preimage` `Mathlib.Data.Finset.SMulAntidiagonal` `Mathlib.Data.Finset.Sym` `Mathlib.Data.Finsupp.Defs` `Mathlib.Data.Finsupp.Fin` `Mathlib.Data.Finsupp.Indicator` `Mathlib.Data.Finsupp.NeLocus` `Mathlib.Data.Finsupp.Notation` `Mathlib.Data.Finsupp.Single` `Mathlib.Data.Fintype.Fin` `Mathlib.Data.Fintype.Option` `Mathlib.Data.Fintype.Order` `Mathlib.Data.Fintype.Pi` `Mathlib.Data.Fintype.Powerset` `Mathlib.Data.Fintype.Prod` `Mathlib.Data.Fintype.Sum` `Mathlib.Data.Fintype.Vector` `Mathlib.Data.FunLike.Fintype` `Mathlib.Data.List.ToFinsupp` `Mathlib.Data.Nat.Lattice` `Mathlib.Data.PNat.Interval` `Mathlib.Data.Set.Countable` `Mathlib.Data.Set.Finite.Basic` `Mathlib.Data.Set.Finite.Lattice` `Mathlib.Data.Set.Finite.Lemmas` `Mathlib.Data.Set.Finite.List` `Mathlib.Data.Set.Finite.Monad` `Mathlib.Data.Set.Finite.Powerset` `Mathlib.Data.Set.MemPartition` `Mathlib.Data.Set.MulAntidiagonal` `Mathlib.Data.Set.SMulAntidiagonal` `Mathlib.Data.Set.Sups` `Mathlib.Data.SetLike.Fintype` `Mathlib.Data.Sigma.Interval` `Mathlib.Data.Sum.Interval` `Mathlib.MeasureTheory.MeasurableSpace.Defs` `Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable` `Mathlib.MeasureTheory.MeasurableSpace.Invariants` `Mathlib.MeasureTheory.PiSystem` `Mathlib.MeasureTheory.SetAlgebra` `Mathlib.MeasureTheory.SetSemiring` `Mathlib.Order.Atoms.Finite` `Mathlib.Order.Birkhoff` `Mathlib.Order.BooleanGenerators` `Mathlib.Order.BooleanSubalgebra` `Mathlib.Order.Category.FinBddDistLat` `Mathlib.Order.Category.FinBoolAlg` `Mathlib.Order.Category.FinPartOrd` `Mathlib.Order.Category.NonemptyFinLinOrd` `Mathlib.Order.CompactlyGenerated.Basic` `Mathlib.Order.CompactlyGenerated.Intervals` `Mathlib.Order.CompleteLattice.SetLike` `Mathlib.Order.CompleteSublattice` `Mathlib.Order.ConditionallyCompleteLattice.Finset` `Mathlib.Order.Disjointed` `Mathlib.Order.Filter.AtTopBot.Basic` `Mathlib.Order.Filter.AtTopBot.CountablyGenerated` `Mathlib.Order.Filter.AtTopBot.Finset` `Mathlib.Order.Filter.Bases` `Mathlib.Order.Filter.Cofinite` `Mathlib.Order.Filter.CountableInter` `Mathlib.Order.Filter.CountableSeparatingOn` `Mathlib.Order.Filter.CountablyGenerated` `Mathlib.Order.Filter.EventuallyConst` `Mathlib.Order.Filter.Finite` `Mathlib.Order.Filter.Interval` `Mathlib.Order.Filter.Lift` `Mathlib.Order.Filter.Pi` `Mathlib.Order.Filter.SmallSets` `Mathlib.Order.Filter.Subsingleton` `Mathlib.Order.Filter.Ultrafilter.Basic` `Mathlib.Order.Interval.Finset.Basic` `Mathlib.Order.Interval.Finset.Defs` `Mathlib.Order.Interval.Finset.Fin` `Mathlib.Order.Interval.Finset.Nat` `Mathlib.Order.Interval.Multiset` `Mathlib.Order.Interval.Set.Infinite` `Mathlib.Order.OrderIsoNat` `Mathlib.Order.PartialSups` `Mathlib.Order.Restriction` `Mathlib.Order.Sublattice` `Mathlib.Order.SupClosed` `Mathlib.Order.UpperLower.LocallyFinite` `Mathlib.Order.WellFoundedSet` `Mathlib.Order.WellQuasiOrder` `Mathlib.RingTheory.HahnSeries.Basic` `Mathlib.RingTheory.Nilpotent.Defs` `Mathlib.SetTheory.Descriptive.Tree` `Mathlib.Tactic.DeriveFintype` `Mathlib.Tactic.RewriteSearch` `Mathlib.Topology.Baire.Lemmas` `Mathlib.Topology.Basic` `Mathlib.Topology.Bornology.Basic` `Mathlib.Topology.Bornology.Hom` `Mathlib.Topology.Category.Born` `Mathlib.Topology.Defs.Induced` `Mathlib.Topology.GDelta.Basic` `Mathlib.Topology.Maps.Basic` `Mathlib.Topology.Maps.OpenQuotient` `Mathlib.Topology.NhdsSet` `Mathlib.Topology.Order.Hom.Basic` `Mathlib.Topology.Order.Hom.Esakia` `Mathlib.Topology.Order` `Mathlib.Topology.Partial` `Mathlib.Topology.Separation.SeparatedNhds` `Mathlib.Topology.Ultrafilter` `Mathlib.Topology.UniformSpace.Defs` `Mathlib.Topology.UniformSpace.OfFun`	-1
959 files `Mathlib.Algebra.BrauerGroup.Defs` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.ModuleCat.ExteriorPower` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Central.TensorProduct` `Mathlib.Algebra.CharP.CharAndCard` `Mathlib.Algebra.DirectSum.LinearMap` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.CartanMatrix` `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.Free` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.InvariantForm` `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.Sl2` `Mathlib.Algebra.Lie.Solvable` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.Algebra.Module.ZMod` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.Algebra.Star.CHSH` `Mathlib.Algebra.Symmetrized` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.Group` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective` `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.AlgebraicTopology.RelativeCellComplex.Basic` `Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.Analysis.AbsoluteValue.Equivalence` `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.Analysis.Analytic.IteratedFDeriv` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.Analytic.OfScalars` `Mathlib.Analysis.Analytic.Order` `Mathlib.Analysis.Analytic.RadiusLiminf` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Multiplier` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.CStarAlgebra.lpSpace` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Analysis.Calculus.Conformal.InnerProduct` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Calculus.Deriv.Add` `Mathlib.Analysis.Calculus.Deriv.AffineMap` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Calculus.Deriv.Linear` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.Calculus.Deriv.Pi` `Mathlib.Analysis.Calculus.Deriv.Polynomial` `Mathlib.Analysis.Calculus.Deriv.Pow` `Mathlib.Analysis.Calculus.Deriv.Prod` `Mathlib.Analysis.Calculus.Deriv.Shift` `Mathlib.Analysis.Calculus.Deriv.Slope` `Mathlib.Analysis.Calculus.Deriv.Star` `Mathlib.Analysis.Calculus.Deriv.Support` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.FDeriv.Linear` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.Pi` `Mathlib.Analysis.Calculus.FDeriv.Prod` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.LagrangeMultipliers` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Topology` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Analysis.Hofer` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Completion` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.InnerProductSpace.Continuous` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.LocallyConvex.AbsConvexOpen` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.MeanInequalitiesPow` `Mathlib.Analysis.MeanInequalities` `Mathlib.Analysis.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Algebra.Norm` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Algebra.UnitizationL1` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.InfiniteSum` `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.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.ControlledClosure` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Int` `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.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Lp.ProdLp` `Mathlib.Analysis.Normed.Lp.lpSpace` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `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.IsPowMulFaithful` `Mathlib.Analysis.Normed.Ring.SeminormFromBounded` `Mathlib.Analysis.Normed.Ring.SeminormFromConst` `Mathlib.Analysis.Normed.Ring.Seminorm` `Mathlib.Analysis.Normed.Ring.SmoothingSeminorm` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Analysis.NormedSpace.Connected` `Mathlib.Analysis.NormedSpace.DualNumber` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Polynomial.Basic` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.Bernstein` `Mathlib.Analysis.SpecialFunctions.Choose` `Mathlib.Analysis.SpecialFunctions.CompareExp` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.Log.Base` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.Analysis.SpecialFunctions.Log.Monotone` `Mathlib.Analysis.SpecialFunctions.Log.PosLog` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics` `Mathlib.Analysis.SpecialFunctions.Pow.Complex` `Mathlib.Analysis.SpecialFunctions.Pow.Continuity` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Analysis.Subadditive` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous` `Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.CategoryTheory.SmallObject.Basic` `Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument` `Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting` `Mathlib.CategoryTheory.SmallObject.TransfiniteIteration` `Mathlib.Combinatorics.Additive.CauchyDavenport` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` `Mathlib.Combinatorics.Configuration` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.SimpleGraph.Clique` `Mathlib.Combinatorics.SimpleGraph.Coloring` `Mathlib.Combinatorics.SimpleGraph.ConcreteColorings` `Mathlib.Combinatorics.SimpleGraph.Partition` `Mathlib.Combinatorics.SimpleGraph.Regularity.Bound` `Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk` `Mathlib.Combinatorics.SimpleGraph.Regularity.Increment` `Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma` `Mathlib.Combinatorics.SimpleGraph.Sum` `Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SimpleGraph.Triangle.Counting` `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite` `Mathlib.Combinatorics.SimpleGraph.Turan` `Mathlib.Combinatorics.SimpleGraph.UniversalVerts` `Mathlib.Computability.AkraBazzi.GrowsPolynomially` `Mathlib.Computability.DFA` `Mathlib.Computability.EpsilonNFA` `Mathlib.Computability.MyhillNerode` `Mathlib.Computability.NFA` `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.Abs` `Mathlib.Data.Complex.Cardinality` `Mathlib.Data.Complex.Determinant` `Mathlib.Data.Complex.Exponential` `Mathlib.Data.Complex.FiniteDimensional` `Mathlib.Data.Complex.Norm` `Mathlib.Data.Complex.Order` `Mathlib.Data.Complex.Orientation` `Mathlib.Data.Complex.Trigonometric` `Mathlib.Data.Matrix.DoublyStochastic` `Mathlib.Data.Matrix.Kronecker` `Mathlib.Data.Matrix.Rank` `Mathlib.Data.Nat.Factorial.SuperFactorial` `Mathlib.Data.Real.Cardinality` `Mathlib.Data.Real.CompleteField` `Mathlib.Data.Real.GoldenRatio` `Mathlib.Data.Real.Hyperreal` `Mathlib.Data.Real.Irrational` `Mathlib.Data.Real.IsNonarchimedean` `Mathlib.Data.Real.Sqrt` `Mathlib.Data.Real.StarOrdered` `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.TopologicalEntropy.CoverEntropy` `Mathlib.Dynamics.TopologicalEntropy.NetEntropy` `Mathlib.Dynamics.TopologicalEntropy.Semiconj` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.ChevalleyWarning` `Mathlib.FieldTheory.Extension` `Mathlib.FieldTheory.Finite.Basic` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.FieldTheory.Fixed` `Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra` `Mathlib.FieldTheory.IntermediateField.Adjoin.Basic` `Mathlib.FieldTheory.IntermediateField.Algebraic` `Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure` `Mathlib.FieldTheory.IsAlgClosed.Basic` `Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.FieldTheory.KummerPolynomial` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.FieldTheory.Minpoly.IsConjRoot` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.MvRatFunc.Rank` `Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure` `Mathlib.FieldTheory.Normal.Defs` `Mathlib.FieldTheory.PerfectClosure` `Mathlib.FieldTheory.Perfect` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.Relrank` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.FieldTheory.Separable` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.FieldTheory.SplittingField.IsSplittingField` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Geometry.Manifold.ChartedSpace` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.Geometry.Manifold.LocalInvariantProperties` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.GroupTheory.FixedPointFree` `Mathlib.GroupTheory.Frattini` `Mathlib.GroupTheory.MonoidLocalization.Cardinality` `Mathlib.GroupTheory.Nilpotent` `Mathlib.GroupTheory.Order.Min` `Mathlib.GroupTheory.OreLocalization.Cardinality` `Mathlib.GroupTheory.PGroup` `Mathlib.GroupTheory.Perm.Centralizer` `Mathlib.GroupTheory.Perm.Cycle.Concrete` `Mathlib.GroupTheory.Perm.Cycle.PossibleTypes` `Mathlib.GroupTheory.Perm.Cycle.Type` `Mathlib.GroupTheory.Perm.Fin` `Mathlib.GroupTheory.Schreier` `Mathlib.GroupTheory.SchurZassenhaus` `Mathlib.GroupTheory.SpecificGroups.Alternating` `Mathlib.GroupTheory.SpecificGroups.ZGroup` `Mathlib.GroupTheory.Sylow` `Mathlib.GroupTheory.Torsion` `Mathlib.GroupTheory.Transfer` `Mathlib.LinearAlgebra.AffineSpace.Matrix` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange` `Mathlib.LinearAlgebra.CliffordAlgebra.Basic` `Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory` `Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation` `Mathlib.LinearAlgebra.CliffordAlgebra.Contraction` `Mathlib.LinearAlgebra.CliffordAlgebra.Equivs` `Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv` `Mathlib.LinearAlgebra.CliffordAlgebra.Even` `Mathlib.LinearAlgebra.CliffordAlgebra.Fold` `Mathlib.LinearAlgebra.CliffordAlgebra.Grading` `Mathlib.LinearAlgebra.CliffordAlgebra.Inversion` `Mathlib.LinearAlgebra.CliffordAlgebra.Prod` `Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup` `Mathlib.LinearAlgebra.CliffordAlgebra.Star` `Mathlib.LinearAlgebra.CrossProduct` `Mathlib.LinearAlgebra.Determinant` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.ExteriorAlgebra.Basic` `Mathlib.LinearAlgebra.ExteriorAlgebra.Grading` `Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating` `Mathlib.LinearAlgebra.ExteriorPower.Basic` `Mathlib.LinearAlgebra.ExteriorPower.Pairing` `Mathlib.LinearAlgebra.FreeModule.Determinant` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.Lagrange` `Mathlib.LinearAlgebra.LinearDisjoint` `Mathlib.LinearAlgebra.Matrix.AbsoluteValue` `Mathlib.LinearAlgebra.Matrix.Adjugate` `Mathlib.LinearAlgebra.Matrix.BaseChange` `Mathlib.LinearAlgebra.Matrix.Basis` `Mathlib.LinearAlgebra.Matrix.BilinearForm` `Mathlib.LinearAlgebra.Matrix.Block` `Mathlib.LinearAlgebra.Matrix.Charpoly.Basic` `Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField` `Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.LinearAlgebra.Matrix.Charpoly.Univ` `Mathlib.LinearAlgebra.Matrix.Determinant.Basic` `Mathlib.LinearAlgebra.Matrix.Determinant.Misc` `Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular` `Mathlib.LinearAlgebra.Matrix.FixedDetMatrices` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.LinearAlgebra.Matrix.IsDiag` `Mathlib.LinearAlgebra.Matrix.MvPolynomial` `Mathlib.LinearAlgebra.Matrix.Nondegenerate` `Mathlib.LinearAlgebra.Matrix.NonsingularInverse` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.Matrix.Polynomial` `Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup` `Mathlib.LinearAlgebra.Matrix.Reindex` `Mathlib.LinearAlgebra.Matrix.SesquilinearForm` `Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup` `Mathlib.LinearAlgebra.Matrix.Swap` `Mathlib.LinearAlgebra.Matrix.ToLinearEquiv` `Mathlib.LinearAlgebra.Matrix.Transvection` `Mathlib.LinearAlgebra.Matrix.ZPow` `Mathlib.LinearAlgebra.Orientation` `Mathlib.LinearAlgebra.PID` `Mathlib.LinearAlgebra.PerfectPairing.Restrict` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.LinearAlgebra.QuadraticForm.Basic` `Mathlib.LinearAlgebra.QuadraticForm.Basis` `Mathlib.LinearAlgebra.QuadraticForm.Dual` `Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv` `Mathlib.LinearAlgebra.QuadraticForm.Isometry` `Mathlib.LinearAlgebra.QuadraticForm.Prod` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct` `Mathlib.LinearAlgebra.SymplecticGroup` `Mathlib.LinearAlgebra.TensorProduct.Matrix` `Mathlib.LinearAlgebra.Trace` `Mathlib.LinearAlgebra.UnitaryGroup` `Mathlib.LinearAlgebra.Vandermonde` `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.Pi` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `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.ConvergenceInMeasure` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.MeasureTheory.Function.LpSpace.Basic` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `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.Integral.Marginal` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic` `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.Doubling` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `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.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.Defs` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.OuterMeasure.OfAddContent` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed` `Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.DiophantineApproximation.Basic` `Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.NumberTheory.FermatPsp` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.NumberTheory.LegendreSymbol.Basic` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.NumberTheory.Ostrowski` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.NumberTheory.Padics.MahlerBasis` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.Pell` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.Rayleigh` `Mathlib.NumberTheory.SumFourSquares` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.NumberTheory.Wilson` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Order.Filter.ENNReal` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Order.JordanHolder` `Mathlib.Order.KonigLemma` `Mathlib.Order.KrullDimension` `Mathlib.Order.RelSeries` `Mathlib.Order.SuccPred.LinearLocallyFinite` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Distributions.Poisson` `Mathlib.Probability.Independence.Basic` `Mathlib.Probability.Independence.Kernel` `Mathlib.Probability.Kernel.Basic` `Mathlib.Probability.Kernel.Composition.Basic` `Mathlib.Probability.Kernel.Composition.CompNotation` `Mathlib.Probability.Kernel.Composition.ParallelComp` `Mathlib.Probability.Kernel.Defs` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Probability.Kernel.Invariance` `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.Character` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.RingTheory.Algebraic.Integral` `Mathlib.RingTheory.AlgebraicIndependent.Adjoin` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis` `Mathlib.RingTheory.Artinian.Algebra` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.ClassGroup` `Mathlib.RingTheory.Complex` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.Ideal` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Derivation.Lie` `Mathlib.RingTheory.Derivation.MapCoeffs` `Mathlib.RingTheory.FiniteLength` `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.Ideal.GoingUp` `Mathlib.RingTheory.Ideal.Height` `Mathlib.RingTheory.IntegralClosure.Algebra.Basic` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LinearDisjoint` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.RingTheory.Localization.Integral` `Mathlib.RingTheory.NoetherNormalization` `Mathlib.RingTheory.Norm.Defs` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.NormTrace` `Mathlib.RingTheory.OreLocalization.Cardinality` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.RingTheory.Polynomial.SeparableDegree` `Mathlib.RingTheory.PowerBasis` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.RingTheory.SimpleModule.Rank` `Mathlib.RingTheory.TensorProduct.Nontrivial` `Mathlib.RingTheory.Trace.Defs` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.RingTheory.Valuation.LocalSubring` `Mathlib.RingTheory.Valuation.Minpoly` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.Defs` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.Domain` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Frobenius` `Mathlib.RingTheory.WittVector.Identities` `Mathlib.RingTheory.WittVector.InitTail` `Mathlib.RingTheory.WittVector.IsPoly` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.RingTheory.WittVector.MulCoeff` `Mathlib.RingTheory.WittVector.MulP` `Mathlib.RingTheory.WittVector.StructurePolynomial` `Mathlib.RingTheory.WittVector.Teichmuller` `Mathlib.RingTheory.WittVector.Truncated` `Mathlib.RingTheory.WittVector.Verschiebung` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.Topology.Baire.CompleteMetrizable` `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.DeltaGenerated` `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.Nobeling` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.Category.Sequential` `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.Connected.LocPathConnected` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.Germ` `Mathlib.Topology.Homotopy.Basic` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Instances.AddCircle` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Instances.Complex` `Mathlib.Topology.Instances.Discrete` `Mathlib.Topology.Instances.ENNReal.Defs` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.ENat` `Mathlib.Topology.Instances.EReal.Lemmas` `Mathlib.Topology.Instances.Int` `Mathlib.Topology.Instances.Irrational` `Mathlib.Topology.Instances.Matrix` `Mathlib.Topology.Instances.NNReal.Defs` `Mathlib.Topology.Instances.NNReal.Lemmas` `Mathlib.Topology.Instances.Nat` `Mathlib.Topology.Instances.PNat` `Mathlib.Topology.Instances.RatLemmas` `Mathlib.Topology.Instances.Rat` `Mathlib.Topology.Instances.Real.Defs` `Mathlib.Topology.Instances.Real.Lemmas` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Topology.KrullDimension` `Mathlib.Topology.Maps.Proper.CompactlyGenerated` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Topology.MetricSpace.HolderNorm` `Mathlib.Topology.MetricSpace.Holder` `Mathlib.Topology.MetricSpace.Kuratowski` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Path` `Mathlib.Topology.Semicontinuous` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.NotNormal` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UnitInterval` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.Hom`	1
764 files `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.CharP.LinearMaps` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.Classical` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Matrix` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `Mathlib.Algebra.Lie.SkewAdjoint` `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.DedekindDomain` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.Presentation.Differentials` `Mathlib.Algebra.Module.Torsion` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.IdealSheaf` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.Analysis.Analytic.Polynomial` `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.ContDiff.RCLike` `Mathlib.Analysis.Calculus.ContDiff.WithLp` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.FDeriv.WithLp` `Mathlib.Analysis.Calculus.FirstDerivativeTest` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Calculus.Implicit` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.OperatorNorm` `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.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.Convex.AmpleSet` `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.Deriv` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.Convex.Measure` `Mathlib.Analysis.Convex.Normed` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Uniform` `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.Convex` `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.OfNorm` `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.LocallyConvex.WeakSpace` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Lp.LpEquiv` `Mathlib.Analysis.Normed.Lp.PiLp` `Mathlib.Analysis.Normed.Module.Complemented` `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.NormedSpace.HahnBanach.Separation` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `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.Deriv` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.FieldTheory.Isaacs` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.SeparableClosure` `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.AnalyticManifold` `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.Basic` `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` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.LinearAlgebra.Dimension.Torsion.Basic` `Mathlib.LinearAlgebra.Dimension.Torsion.Finite` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.LinearAlgebra.JordanChevalley` `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.QuadraticForm.Complex` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.LinearAlgebra.Reflection` `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.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.OfBilinear` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `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.Lebesgue` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable` `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.ContinuousMapDense` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.MeasureTheory.Function.L1Space.AEEqFun` `Mathlib.MeasureTheory.Function.L1Space.Integrable` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.MeasureTheory.Function.LocallyIntegrable` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous` `Mathlib.MeasureTheory.Function.SimpleFuncDenseLp` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp` `Mathlib.MeasureTheory.Function.UnifTight` `Mathlib.MeasureTheory.Function.UniformIntegrable` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.MeasureTheory.Group.Integral` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.BochnerL1` `Mathlib.MeasureTheory.Integral.Bochner` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `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.IntegrableOn` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Integral.Periodic` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.MeasureTheory.Integral.SetIntegral` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Integral.VitaliCaratheodory` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `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.SeparableMeasure` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.Bertrand` `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.DirichletCharacter.Orthogonality` `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.EulerMascheroni` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.NumberTheory.JacobiSum.Basic` `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.GaussEisensteinLemmas` `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.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.Identities` `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.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.MulChar.Lemmas` `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.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.SumTwoSquares` `Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.ZetaValues` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `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.Integrable` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Integration` `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.Integral` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Probability.Kernel.RadonNikodym` `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.IntegrableExpMul` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Notation` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `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.Maschke` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.AdicCompletion.Exactness` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.Etale.Basic` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Etale.Pi` `Mathlib.RingTheory.Extension` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Generators` `Mathlib.RingTheory.HopkinsLevitzki` `Mathlib.RingTheory.Ideal.Cotangent` `Mathlib.RingTheory.Ideal.GoingDown` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.Invariant` `Mathlib.RingTheory.Jacobson.Ring` `Mathlib.RingTheory.Kaehler.Basic` `Mathlib.RingTheory.Kaehler.CotangentComplex` `Mathlib.RingTheory.Kaehler.JacobiZariski` `Mathlib.RingTheory.Kaehler.Polynomial` `Mathlib.RingTheory.Kaehler.TensorProduct` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Norm.Basic` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.Perfection` `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.Hermite.Gaussian` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.Presentation` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.RingTheory.Regular.RegularSequence` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.Smooth.StandardSmoothCotangent` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.RingTheory.Spectrum.Maximal.Topology` `Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC` `Mathlib.RingTheory.Spectrum.Prime.Jacobson` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Spectrum.Prime.Noetherian` `Mathlib.RingTheory.Spectrum.Prime.Polynomial` `Mathlib.RingTheory.Spectrum.Prime.TensorProduct` `Mathlib.RingTheory.Spectrum.Prime.Topology` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.CWComplex.Abstract.Basic` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.MetricSpace.HausdorffDimension`	2
`Mathlib.Algebra.Group.TypeTags.Fintype`	16
`Mathlib.Data.Fintype.EquivFin` (new file)	458
`Mathlib.Data.Fintype.Pigeonhole` (new file)	479

Declarations diff

+ Set.instFinite
+ instance [Nonempty α] : NeZero (card α) := ⟨card_ne_zero⟩
- Finite.instSet
- Fintype.card_quotient_lt

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

mathlib4-dependent-issues-bot · 2025-02-17T18:36:25Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Data/Fintype): split Data/Fintype/Basic.lean #21831~~
By Dependent Issues (🤖). Happy coding!

j-loreaux · 2025-02-18T22:31:27Z

I'm confused, how did the dependencies for Mathlib.Algebra.Group.TypeTags.Fintype increase due to the split (by 16, when the split was only 4-way)?

Vierkantor · 2025-02-19T17:02:49Z

I'm confused, how did the dependencies for Mathlib.Algebra.Group.TypeTags.Fintype increase due to the split (by 16, when the split was only 4-way)?

I redid the import order so TypeTags.Fintype now imports Fintype.Card instead of the other way around. Although Fintype.Card reduced from 478 to 423 imports, that's still more than Fintype.OfMap used to have.

Vierkantor · 2025-02-19T17:03:41Z

I think since TypeTags.Fintype didn't cause any downstream increases, one +16 is a fine tradeoff for the other decreases.

YaelDillies

Thanks!

maintainer delegate

YaelDillies · 2025-02-19T17:48:28Z

+theorem Fintype.card_fin_lt_of_le {m n : ℕ} (h : m ≤ n) :
+    Fintype.card {i : Fin n // i < m} = m := by
+  conv_rhs => rw [← Fintype.card_fin m]
+  apply Fintype.card_congr
+  exact { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
+          invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩
+          left_inv := fun i ↦ rfl
+          right_inv := fun i ↦ rfl }
+
+theorem Finset.card_fin (n : ℕ) : #(univ : Finset (Fin n)) = n := by simp
+
+/-- `Fin` as a map from `ℕ` to `Type` is injective. Note that since this is a statement about
+equality of types, using it should be avoided if possible. -/
+theorem fin_injective : Function.Injective Fin := fun m n h =>
+  (Fintype.card_fin m).symm.trans <| (Fintype.card_congr <| Equiv.cast h).trans (Fintype.card_fin n)
+
+theorem Fin.val_eq_val_of_heq {k l : ℕ} {i : Fin k} {j : Fin l} (h : HEq i j) :
+    (i : ℕ) = (j : ℕ) :=
+  (Fin.heq_ext_iff (fin_injective (type_eq_of_heq h))).1 h
+
+/-- A reversed version of `Fin.cast_eq_cast` that is easier to rewrite with. -/
+theorem Fin.cast_eq_cast' {n m : ℕ} (h : Fin n = Fin m) :
+    _root_.cast h = Fin.cast (fin_injective h) := by
+  cases fin_injective h
+  rfl


All of this can be moved earlier, I believe

You are completely correct, these now live together with Fintype.card_fin into their own section in Fintype.Card.

github-actions · 2025-02-19T17:50:19Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

bryangingechen · 2025-02-19T18:07:23Z

Thanks!
bors d+

mathlib-bors · 2025-02-19T18:07:27Z

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

This PR splits `Data.Fintype.Card` based on dependencies: * `Data.Fintype.Card` contains the definition of `Fintype.card` and basic results * `Data.Fintype.EquivFin` contains the equivalences between fintypes, finiteness and `Fin` * `Data.Fintype.Pigeonhole` contains a few pigeonhole principles * `Data.Fintype.Group` gets a few extra results on `Additive`/`Multiplicative`

Vierkantor · 2025-02-20T08:45:39Z

Build passed, so let's merge this before more conflicts arise!

bors merge

This PR splits `Data.Fintype.Card` based on dependencies: * `Data.Fintype.Card` contains the definition of `Fintype.card` and basic results * `Data.Fintype.EquivFin` contains the equivalences between fintypes, finiteness and `Fin` * `Data.Fintype.Pigeonhole` contains a few pigeonhole principles * `Data.Fintype.Group` gets a few extra results on `Additive`/`Multiplicative`

mathlib-bors · 2025-02-20T10:03:18Z

Pull request successfully merged into master.

Build succeeded:

…21866) This PR aims to define `Finset.card` and `Fintype.card` without importing anything from the algebra library. In addition to the changes of #21840, we modify a few proofs and move a few lemmas so that `Data.Finset.Card` doesn't need to know about monoids. Co-authored-by: Anne Baanen <[email protected]>

* origin/master: (823 commits) chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) style(Geometry/Manifold): remove superfluous indentation in doc-strings (#22117) chore: rename PushNeg.lean to Push.lean (#22108) feat: add Is{Open,Closed}Embedding.sum_elim (#22070) feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt (#21563) feature(Topology/Algebra/Module/WeakBilin): Linear map from F into the topological dual of E with the weak topology (#21078) feat(CategoryTheory/Abelian): the exact sequence attached to a pushout square (#22110) chore(ChartedSpace.lean): group constructions together (#22107) feat(CategoryTheory/MorphismProperty): more basic API (#22099) chore(Data/Fintype): split `Fintype/Card.lean` (#21840) chore(SetTheory/Cardinal/Cofinality): make `IsStrongLimit` into a structure (#21971) feat(Combinatorics/SimpleGraph): Add a theorem about cliques in induced subgraphs (#20705) ...

Vierkantor added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-data Data (lists, quotients, numbers, etc) labels Feb 13, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 13, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2025

Vierkantor force-pushed the split-Fintype.Card branch from f0a99a0 to ac3904e Compare February 14, 2025 09:38

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 14, 2025

Vierkantor mentioned this pull request Feb 14, 2025

[Merged by Bors] - chore(Data/Finset): don't import algebra when defining Finset.card #21866

Closed

1 task

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 14, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 14, 2025

YaelDillies reviewed Feb 16, 2025

View reviewed changes

Comment thread Mathlib/Data/Fintype/Pigeonhole.lean Outdated

Comment thread Mathlib/Data/Fintype/Powerset.lean Outdated

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 17, 2025

Vierkantor force-pushed the split-Fintype.Card branch from 1f4b347 to c05c11e Compare February 18, 2025 14:52

github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 18, 2025

YaelDillies reviewed Feb 18, 2025

View reviewed changes

Comment thread Mathlib/Data/Fintype/EquivFin.lean Outdated

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2025

Vierkantor removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2025

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2025

Vierkantor removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 19, 2025

YaelDillies approved these changes Feb 19, 2025

View reviewed changes

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

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

ghost removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 19, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2025

Vierkantor added 9 commits February 20, 2025 09:00

Shake

ebb55c2

More shaking

fc2bdc8

Shake

1a8337e

Yaël's suggestions

24570b8

Renamed files

fedc3fe

Fix imports

2c76b4b

Upstream cardinality of Fin

a0c67ba

Move Fin results to their own section in Fintype.Card

811f6c1

Vierkantor force-pushed the split-Fintype.Card branch from e7af4d3 to 811f6c1 Compare February 20, 2025 08:00

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2025

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

mathlib-bors bot changed the title ~~chore(Data/Fintype): split Fintype/Card.lean~~ [Merged by Bors] - chore(Data/Fintype): split Fintype/Card.lean Feb 20, 2025

mathlib-bors bot closed this Feb 20, 2025

mathlib-bors bot deleted the split-Fintype.Card branch February 20, 2025 10:03

Conversation

Vierkantor commented Feb 13, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 811f6c1679

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Feb 17, 2025

Uh oh!

Uh oh!

j-loreaux commented Feb 18, 2025

Uh oh!

Vierkantor commented Feb 19, 2025

Uh oh!

Vierkantor commented Feb 19, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 19, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor Feb 19, 2025

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 19, 2025

Uh oh!

bryangingechen commented Feb 19, 2025

Uh oh!

mathlib-bors bot commented Feb 19, 2025

Uh oh!

Vierkantor commented Feb 20, 2025

Uh oh!

mathlib-bors bot commented Feb 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Vierkantor commented Feb 13, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Feb 14, 2025 •

edited

Loading