Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor: Abstract out the substructure lattice construction and SetLike closure operators #20836

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

artie2000
Copy link
Collaborator


Open in Gitpod

Copy link

PR summary 193a95d84d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
2875 files Mathlib.Algebra.Algebra.Basic Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Algebra.Field Mathlib.Algebra.Algebra.Hom.Rat Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Spectrum Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Algebra.ZMod Mathlib.Algebra.AlgebraicCard Mathlib.Algebra.BigOperators.Associated Mathlib.Algebra.BigOperators.Finsupp Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence Mathlib.Algebra.Category.CoalgebraCat.Monoidal Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.Colimits Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.MonCat.FilteredColimits Mathlib.Algebra.Category.MonCat.Limits Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.Limits Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero Mathlib.Algebra.CharP.Quotient Mathlib.Algebra.CharP.Subring Mathlib.Algebra.CharP.Two Mathlib.Algebra.CharZero.Quotient Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.Module Mathlib.Algebra.Colimit.Ring Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.CubicDiscriminant Mathlib.Algebra.DirectSum.AddChar Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Idempotents Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.LinearMap Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.DualNumber Mathlib.Algebra.DualQuaternion Mathlib.Algebra.Equiv.TransferInstance Mathlib.Algebra.Exact Mathlib.Algebra.Field.Subfield.Basic Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Group.AddChar Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Group.Graph Mathlib.Algebra.Group.Subgroup.Actions Mathlib.Algebra.Group.Subgroup.Basic Mathlib.Algebra.Group.Subgroup.Finite Mathlib.Algebra.Group.Subgroup.Finsupp Mathlib.Algebra.Group.Subgroup.Ker Mathlib.Algebra.Group.Subgroup.Lattice Mathlib.Algebra.Group.Subgroup.Map Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas Mathlib.Algebra.Group.Subgroup.MulOpposite Mathlib.Algebra.Group.Subgroup.Order Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Algebra.Group.Subgroup.ZPowers.Basic Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.Finsupp Mathlib.Algebra.Group.Submonoid.Membership Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.GroupWithZero.NonZeroDivisors Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Lie.Abelian Mathlib.Algebra.Lie.BaseChange Mathlib.Algebra.Lie.Basic Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanMatrix Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Classical Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Algebra.Lie.Derivation.Killing 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.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.Lie.Normalizer Mathlib.Algebra.Lie.OfAssociative Mathlib.Algebra.Lie.Quotient Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Algebra.Lie.Sl2 Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.Subalgebra Mathlib.Algebra.Lie.Submodule Mathlib.Algebra.Lie.TensorProduct Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.UniversalEnveloping 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.LinearRecurrence Mathlib.Algebra.ModEq Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.Injective Mathlib.Algebra.Module.Lattice Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.Finite Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Basic Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.Module.Submodule.Defs Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.Invariant Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Order Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.Module.Submodule.Range Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.Algebra.Module.Torsion Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Module.ZMod Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Comap Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Division Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Order.Chebyshev Mathlib.Algebra.Order.Floor.Div Mathlib.Algebra.Order.Floor.Prime Mathlib.Algebra.Order.Ring.Star Mathlib.Algebra.Order.Star.Basic Mathlib.Algebra.Order.Star.Conjneg Mathlib.Algebra.Order.Star.Prod Mathlib.Algebra.Order.ToIntervalMod Mathlib.Algebra.Periodic Mathlib.Algebra.Pointwise.Stabilizer Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.Expand Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.Splits Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.PresentedMonoid.Basic Mathlib.Algebra.QuaternionBasis Mathlib.Algebra.Quaternion Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Ring.NegOnePow Mathlib.Algebra.Ring.Semireal.Defs Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Algebra.Ring.Subring.Units Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.Ring.SumsOfSquares Mathlib.Algebra.RingQuot Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.Small.Group Mathlib.Algebra.Small.Module Mathlib.Algebra.Small.Ring Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.CHSH Mathlib.Algebra.Star.CentroidHom Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.NonUnitalSubsemiring Mathlib.Algebra.Star.RingQuot Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Star.Subsemiring Mathlib.Algebra.Star.Unitary Mathlib.Algebra.Symmetrized Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing 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.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.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology 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.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex 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.Meromorphic Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.Exponential 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.Module.Synonym Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.AddTorsor.AffineMap 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.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.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Abs 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.Extend Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap 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.MeanValue Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.IntegerCompl Mathlib.Analysis.Complex.IsIntegral 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.ReImTopology Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UnitDisc.Basic 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.ConstantSpeed Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Between Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Normed Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.Radon Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.StoneSeparation Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Convex.Visible 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.Hofer Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal 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.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space 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.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Matrix Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.Constructions 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.Submodule Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.MulAction 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.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra 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.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.HahnBanach.Extension Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.NormedSpace.Int Mathlib.Analysis.NormedSpace.MStructure 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.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.Seminorm Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Analysis.SpecialFunctions.Exponential 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.Base Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv 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.SumIntegralComparisons Mathlib.Analysis.SumOverResidueClass Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckCategory Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.CategoryTheory.Abelian.Injective Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.ProjectiveResolution Mathlib.CategoryTheory.Abelian.Projective Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Action.Concrete Mathlib.CategoryTheory.Action.Continuous Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Action Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Limits.Shapes.SingleObj Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.ProjectiveResolution Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.ApproximateSubgroup Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Additive.VerySmallDoubling Mathlib.Combinatorics.Configuration Mathlib.Combinatorics.Derangements.Basic Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Derangements.Finite Mathlib.Combinatorics.Enumerative.Bell Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Computability.TMComputable 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.ExponentialBounds Mathlib.Data.Complex.Exponential Mathlib.Data.Complex.FiniteDimensional Mathlib.Data.Complex.Module Mathlib.Data.Complex.Order Mathlib.Data.Complex.Orientation Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Ext Mathlib.Data.DFinsupp.Interval Mathlib.Data.DFinsupp.Multiset Mathlib.Data.DFinsupp.Submonoid Mathlib.Data.Finset.Finsupp Mathlib.Data.Finsupp.AList Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Basic Mathlib.Data.Finsupp.Encodable Mathlib.Data.Finsupp.Ext Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Data.Finsupp.Weight Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Int.Star Mathlib.Data.Matrix.Auto Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.ConjTranspose Mathlib.Data.Matrix.DoublyStochastic Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Hadamard Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Kronecker Mathlib.Data.Matrix.Notation Mathlib.Data.Matrix.Rank Mathlib.Data.Matrix.Reflection Mathlib.Data.Matrix.RowCol Mathlib.Data.Multiset.Interval Mathlib.Data.Nat.Choose.Cast Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Choose.Lucas Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Data.Nat.Factorial.Cast Mathlib.Data.Nat.Factorial.SuperFactorial Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Data.Nat.Periodic Mathlib.Data.Nat.Squarefree Mathlib.Data.Nat.Totient Mathlib.Data.Rat.Star 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.Pi.Bounds Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Data.Real.Sqrt Mathlib.Data.Real.StarOrdered Mathlib.Data.ZMod.Aut Mathlib.Data.ZMod.Basic Mathlib.Data.ZMod.Coprime Mathlib.Data.ZMod.Factorial Mathlib.Data.ZMod.IntUnitsPower Mathlib.Data.ZMod.Quotient Mathlib.Data.ZMod.Units Mathlib.Deprecated.Subfield Mathlib.Deprecated.Subgroup Mathlib.Deprecated.Subring Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Conservative Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Dynamics.Ergodic.Function Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Dynamics.Flow Mathlib.Dynamics.Minimal Mathlib.Dynamics.Newton Mathlib.Dynamics.OmegaLimit Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.FieldTheory.AbelRuffini Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.AlgebraicClosure Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.CardinalEmb Mathlib.FieldTheory.Cardinality Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.Differential.Basic Mathlib.FieldTheory.Differential.Liouville Mathlib.FieldTheory.Extension Mathlib.FieldTheory.Finite.Basic Mathlib.FieldTheory.Finite.GaloisField Mathlib.FieldTheory.Finite.Polynomial Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Finiteness Mathlib.FieldTheory.Fixed Mathlib.FieldTheory.Galois.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.IntermediateField.Adjoin.Defs Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.FieldTheory.IntermediateField.Basic Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.FieldTheory.IsPerfectClosure Mathlib.FieldTheory.IsSepClosed Mathlib.FieldTheory.Isaacs Mathlib.FieldTheory.JacobsonNoether Mathlib.FieldTheory.KrullTopology Mathlib.FieldTheory.KummerExtension Mathlib.FieldTheory.KummerPolynomial Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Minpoly.Field Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.FieldTheory.MvRatFunc.Rank Mathlib.FieldTheory.NormalClosure Mathlib.FieldTheory.Normal Mathlib.FieldTheory.PerfectClosure Mathlib.FieldTheory.Perfect Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.PrimitiveElement Mathlib.FieldTheory.PurelyInseparable Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Basic Mathlib.FieldTheory.RatFunc.Defs Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.Relrank Mathlib.FieldTheory.SeparableClosure Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.FieldTheory.Tower Mathlib.Geometry.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.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.PerpBisector 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.Group.Growth.QuotientInter 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.ChartedSpace Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.ContMDiff.Product 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.InteriorBoundary Mathlib.Geometry.Manifold.IsManifold Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.LocalInvariantProperties 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.Basic 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.WhitneyEmbedding Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.GroupTheory.Abelianization Mathlib.GroupTheory.ArchimedeanDensely Mathlib.GroupTheory.Archimedean Mathlib.GroupTheory.ClassEquation Mathlib.GroupTheory.Commensurable Mathlib.GroupTheory.Commutator.Basic Mathlib.GroupTheory.Commutator.Finite Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.Complement Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Coprod.Basic Mathlib.GroupTheory.CoprodI Mathlib.GroupTheory.Coset.Basic Mathlib.GroupTheory.Coset.Card Mathlib.GroupTheory.Coset.Defs Mathlib.GroupTheory.CosetCover Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.Divisible Mathlib.GroupTheory.DoubleCoset Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.Finiteness Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.Frattini Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.GroupTheory.FreeAbelianGroup Mathlib.GroupTheory.FreeGroup.Basic Mathlib.GroupTheory.FreeGroup.IsFreeGroup Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.GroupTheory.FreeGroup.Reduce Mathlib.GroupTheory.Goursat Mathlib.GroupTheory.GroupAction.Basic Mathlib.GroupTheory.GroupAction.Blocks Mathlib.GroupTheory.GroupAction.CardCommute Mathlib.GroupTheory.GroupAction.ConjAct Mathlib.GroupTheory.GroupAction.Defs Mathlib.GroupTheory.GroupAction.FixedPoints Mathlib.GroupTheory.GroupAction.FixingSubgroup Mathlib.GroupTheory.GroupAction.Period Mathlib.GroupTheory.GroupAction.Quotient Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise Mathlib.GroupTheory.GroupAction.SubMulAction Mathlib.GroupTheory.GroupExtension.Defs Mathlib.GroupTheory.HNNExtension Mathlib.GroupTheory.Index Mathlib.GroupTheory.MonoidLocalization.Away Mathlib.GroupTheory.MonoidLocalization.Basic Mathlib.GroupTheory.MonoidLocalization.Cardinality Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero Mathlib.GroupTheory.MonoidLocalization.Order Mathlib.GroupTheory.Nilpotent Mathlib.GroupTheory.NoncommPiCoprod Mathlib.GroupTheory.Order.Min Mathlib.GroupTheory.OrderOfElement Mathlib.GroupTheory.OreLocalization.Basic Mathlib.GroupTheory.OreLocalization.Cardinality Mathlib.GroupTheory.PGroup Mathlib.GroupTheory.Perm.ClosureSwap Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.ConjAct Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.DomMulAct Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.Perm.Finite Mathlib.GroupTheory.Perm.Option Mathlib.GroupTheory.Perm.Sign Mathlib.GroupTheory.Perm.Subgroup Mathlib.GroupTheory.PresentedGroup Mathlib.GroupTheory.PushoutI Mathlib.GroupTheory.QuotientGroup.Basic Mathlib.GroupTheory.QuotientGroup.Defs Mathlib.GroupTheory.QuotientGroup.Finite Mathlib.GroupTheory.Schreier Mathlib.GroupTheory.SchurZassenhaus Mathlib.GroupTheory.SemidirectProduct Mathlib.GroupTheory.Solvable Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.GroupTheory.Subgroup.Center Mathlib.GroupTheory.Subgroup.Centralizer Mathlib.GroupTheory.Subgroup.Saturated Mathlib.GroupTheory.Subgroup.Simple Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Submonoid.Inverses Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.GroupTheory.Sylow Mathlib.GroupTheory.Torsion Mathlib.GroupTheory.Transfer Mathlib.InformationTheory.Hamming Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.LinearAlgebra.Basis.Defs Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Coevaluation Mathlib.LinearAlgebra.Contraction Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.Dimension.ErdosKaplansky Mathlib.LinearAlgebra.Dimension.Finite Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.LinearAlgebra.Dimension.Free Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.LinearAlgebra.Dimension.Localization Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Dimension.StrongRankCondition Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Dual Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.LinearAlgebra.ExteriorPower.Pairing Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.LinearAlgebra.FiniteDimensional Mathlib.LinearAlgebra.FiniteSpan Mathlib.LinearAlgebra.Finsupp.Defs Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.SumProd Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeAlgebra Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.FreeModule.PID Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.LinearAlgebra.Isomorphisms Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.Lagrange Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.LinearIndependent Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.Ideal Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.PerfectPairing.Basic Mathlib.LinearAlgebra.PerfectPairing.Restrict Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.LinearAlgebra.QuadraticForm.Complex 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.Real Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Defs Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.Reflection Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic 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.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.LinearAlgebra.SModEq Mathlib.LinearAlgebra.Semisimple Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.Span.Defs Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Quotient Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.LinearAlgebra.Trace Mathlib.LinearAlgebra.UnitaryGroup Mathlib.LinearAlgebra.Vandermonde Mathlib.Logic.Equiv.Fintype Mathlib.Logic.Hydra Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.AddChar Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Constructions.SubmoduleQuotient 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.Covering.VitaliFamily Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.AEMeasurableSequence 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.ConvergenceInMeasure Mathlib.MeasureTheory.Function.Egorov Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable 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.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Function.SimpleFuncDenseLp 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.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.Defs Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Pointwise Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average 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.Indicator Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.MeasureTheory.MeasurableSpace.Pi Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict Mathlib.MeasureTheory.MeasurableSpace.Prod Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.MeasureTheory.Measure.Comap Mathlib.MeasureTheory.Measure.Complex Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.Count Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Measure.Doubling Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic 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.HasOuterApproxClosed 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.Map Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Sub Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.Order.UpperLower 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.OfFunction Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.Basic Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter 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.Dioph Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.EulerProduct.Basic Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Basic Mathlib.NumberTheory.FLT.Four Mathlib.NumberTheory.FLT.MasonStothers Mathlib.NumberTheory.FLT.Polynomial Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.FermatPsp Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FrobeniusNumber Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.LucasPrimality Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.CongruenceSubgroups 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.Basic Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.MulChar.Lemmas Mathlib.NumberTheory.Multiplicity 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.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.PellMatiyasevic Mathlib.NumberTheory.Pell Mathlib.NumberTheory.PrimeCounting Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.Primorial Mathlib.NumberTheory.PythagoreanTriples Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.Rayleigh Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SmoothNumbers Mathlib.NumberTheory.SumFourSquares Mathlib.NumberTheory.SumPrimeReciprocals 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.VonMangoldt Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.Wilson Mathlib.NumberTheory.ZetaValues Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Order.Filter.ENNReal Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.ConditionalExpectation Mathlib.Probability.ConditionalProbability Mathlib.Probability.Density Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson Mathlib.Probability.Distributions.Uniform Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.Kernel Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Integration Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.Basic Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Defs 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.MeasurableStieltjes Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper 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 Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.ProbabilityMassFunction.Monad 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.UniformOn Mathlib.Probability.Variance Mathlib.RepresentationTheory.Basic Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Maschke Mathlib.RepresentationTheory.Rep Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.AdicCompletion.Basic Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.Adjoin.Dimension Mathlib.RingTheory.Adjoin.FG Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.Adjoin.Tower Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Algebraic.Basic Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.RingTheory.Artinian.Instances Mathlib.RingTheory.Artinian.Module Mathlib.RingTheory.Artinian.Ring Mathlib.RingTheory.Bezout Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Binomial Mathlib.RingTheory.ChainOfDivisors Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.Complex Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Opposite Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.Derivation.Lie Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Discriminant Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DualNumber Mathlib.RingTheory.EisensteinCriterion Mathlib.RingTheory.EssentialFiniteness Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Extension Mathlib.RingTheory.Filtration Mathlib.RingTheory.FiniteLength Mathlib.RingTheory.FinitePresentation Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.FiniteType Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Finiteness.Ideal Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Finiteness.Nakayama Mathlib.RingTheory.Finiteness.Nilpotent Mathlib.RingTheory.Finiteness.Prod Mathlib.RingTheory.Finiteness.Projective Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.RingTheory.Finiteness.TensorProduct Mathlib.RingTheory.Fintype Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.FreeRing Mathlib.RingTheory.Generators Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Henselian Mathlib.RingTheory.HopfAlgebra Mathlib.RingTheory.Ideal.AssociatedPrime Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Ideal.Basis Mathlib.RingTheory.Ideal.BigOperators Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Ideal.Defs Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.RingTheory.Ideal.IsPrimary Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.Ideal.Lattice Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.MinimalPrime Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prime Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Ideal.Quotient.Basic Mathlib.RingTheory.Ideal.Quotient.Defs Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.Ideal.Quotient.Noetherian Mathlib.RingTheory.Ideal.Quotient.Operations Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.Idempotents Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IntegralDomain Mathlib.RingTheory.Invariant Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.IsPrimary Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.Jacobson.Ideal Mathlib.RingTheory.Jacobson.Polynomial Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.KrullDimension.Basic Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.Lasker Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.Localization.Algebra Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.Localization.Away.Lemmas Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.Cardinality Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.Ideal Mathlib.RingTheory.Localization.Integer Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.Localization.Submodule Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MvPolynomial.Basic Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.MvPolynomial Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Nakayama Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Noetherian.Basic Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Noetherian.Orzech Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.RingTheory.Norm.Basic Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Norm.Transitivity Mathlib.RingTheory.NormTrace Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OreLocalization.Basic Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.OreLocalization.Ring Mathlib.RingTheory.OrzechProperty Mathlib.RingTheory.Perfection Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Polynomial.Basic Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.Polynomial.Content Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Dickson Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.Quotient Mathlib.RingTheory.Polynomial.Radical Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.Presentation Mathlib.RingTheory.PrincipalIdealDomainOfPrime Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.Radical Mathlib.RingTheory.ReesAlgebra Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.SimpleModule Mathlib.RingTheory.SimpleRing.Basic Mathlib.RingTheory.SimpleRing.Defs Mathlib.RingTheory.SimpleRing.Field Mathlib.RingTheory.SimpleRing.Matrix Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Maximal.Basic Mathlib.RingTheory.Spectrum.Maximal.Defs Mathlib.RingTheory.Spectrum.Maximal.Topology Mathlib.RingTheory.Spectrum.Prime.Basic Mathlib.RingTheory.Spectrum.Prime.Defs 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.Support Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Finite Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.TwoSidedIdeal.Basic Mathlib.RingTheory.TwoSidedIdeal.BigOperators Mathlib.RingTheory.TwoSidedIdeal.Instances Mathlib.RingTheory.TwoSidedIdeal.Kernel Mathlib.RingTheory.TwoSidedIdeal.Lattice Mathlib.RingTheory.TwoSidedIdeal.Operations Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.Defs Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Archimedean Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.Quotient Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValExtension Mathlib.RingTheory.Valuation.ValuationRing Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.WittVector.Basic Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Defs Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.WittVector.Identities Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.WittVector.Isocrystal Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.WittVector.MulP Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.WittVector.Teichmuller Mathlib.RingTheory.WittVector.Truncated Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.RingTheory.ZMod Mathlib.SetTheory.Cardinal.Finsupp Mathlib.SetTheory.Cardinal.Free Mathlib.SetTheory.Cardinal.Subfield Mathlib.SetTheory.Nimber.Field Mathlib.SetTheory.Surreal.Dyadic Mathlib.SetTheory.Surreal.Multiplication Mathlib.Tactic.Algebraize Mathlib.Tactic.ComputeDegree Mathlib.Tactic.FunProp.ContDiff Mathlib.Tactic.FunProp.Differentiable Mathlib.Tactic.Module Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic.ReduceModChar Mathlib.Tactic Mathlib.Testing.Plausible.Functions Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Algebra.ClosedSubgroup Mathlib.Topology.Algebra.ConstMulAction Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.Algebra.GroupCompletion Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Topology.Algebra.Module.Compact Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.Simple Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.Module.WeakBilin Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.MulAction Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Order.Archimedean Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.Floor Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformGroup.Basic Mathlib.Topology.Algebra.UniformGroup.Defs Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.CWComplex 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.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.Compactification.OnePointEquiv Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.Connected.PathConnected Mathlib.Topology.ContinuousMap.Algebra 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.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.Star 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.ENNReal.Defs Mathlib.Topology.Instances.ENNReal.Lemmas Mathlib.Topology.Instances.ENat Mathlib.Topology.Instances.EReal.Defs Mathlib.Topology.Instances.EReal.Lemmas Mathlib.Topology.Instances.Irrational Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.NNReal.Defs Mathlib.Topology.Instances.NNReal.Lemmas 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.TrivSqZeroExt Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.List Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.MetricSpace.Contracting Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Topology.MetricSpace.Lipschitz 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.Bounded Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.PartitionOfUnity Mathlib.Topology.Semicontinuous Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.Separation.NotNormal Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.TietzeExtension Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UniformSpace.Matrix Mathlib.Topology.UnitInterval Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.Hom
1
Mathlib.Data.SetLike.Closure (new file) 271

Declarations diff

+ HasClosure
+ IsConcreteClosure
+ IsConcreteLE
+ IsConcreteSInf
+ _
+ closure_eq_sInf
+ closure_monotone
+ coe_bot
+ coe_closure
+ coe_mono
+ coe_monotone
+ instance : HasClosure (Subsemigroup M) M := SetLike.toHasClosure (Subsemigroup M) M
+ instance : IsConcreteLE L α
+ instance : IsConcreteSInf (Subsemigroup M) M
+ instance : IsConcreteSInf L α
+ instance : PartialOrder (Subsemigroup M) := SetLike.toPartialOrder (Subsemigroup M) M
+ instance [CompleteLattice A] [IsConcreteSInf A B] : IsConcreteClosure A B
+ isGLB_closure
+ l_le_l_iff_le
+ le_of_l_le_l
+ le_of_u_le_u
+ mem_bot
+ mem_closure_of_mem
+ mem_of_le_of_mem
+ toCompleteLattice
+ toCompleteLattice_abstract
+ toHasClosure
+ toLE
+ toPartialOrder
+ u_le_u_iff_le
++ instance : IsConcreteLE A B
- gi
- instance (priority := 100) instPartialOrder : PartialOrder A

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant