Skip to content

chore: migrate to tfae block tactic - #11003

Draft
thorimur wants to merge 55 commits into
masterfrom
tfae-block-syntax-update
Draft

chore: migrate to tfae block tactic#11003
thorimur wants to merge 55 commits into
masterfrom
tfae-block-syntax-update

Conversation

@thorimur

@thorimur thorimur commented Feb 27, 2024 •
edited
Loading

Copy link
Copy Markdown
Contributor

Migrates to the tfae block tactic syntax, eliminating uses of tfae_have and tfae_finish.

Open in Gitpod

@thorimur
feat: := syntax
7c0f799
@thorimur
docs: update to include := syntax
fb4846a
@thorimur
chore: style, test comments/refinement
5c0b6f7
@thorimur
fix: mimic have behavior more faithfully
d684d17
@thorimur
refactor, feat: use have directly for tfae_have
60abee2
@thorimur
feat: re-support Mathlib have
fbbad64
@thorimur
chore: clean up hover text
d37994f
@thorimur
test: new tests, update syntax
bc4fd75
@thorimur
syntax: change tfae_have i <arr> j to tfae_have : i <arr> j
fba28f5
@thorimur
chore: banish tfae_have ... exact
62c2d6a
@thorimur
chore: reduce tfae_have ... intro in favor of pattern matching
58de6a1
@thorimur
chore: banish "mathlib have"-style syntax
9973ad6
@thorimur
chore: fix porting note?
36f2911
@thorimur
chore: newly unused variable
e0c928a
@thorimur
style: clean up types/parses, remove docstrings from parsers to preve…
5a97360 
…nt them appearing on hover
@thorimur
Merge branch 'tfae-have-stx-tweak' into tfae-chore-syntax-update
e688701
@thorimur
chore: revert tfae_have : 1 → 2 syntax to tfae_have 1 → 2
32ba7da
@thorimur
Revert "syntax: change tfae_have i <arr> j to tfae_have : i <arr> j"
b128a07 
This reverts commit fba28f5.
@thorimur
test: revert : syntax
bdf07b8
@thorimur
chore: revert : syntax in docstrings
547af66
@thorimur
chore: noshake Mathlib.Tactic.Have import for TFAE
87c4a45
@thorimur
chore: account for nested comments in lint-style.py
1727e22
@thorimur
chore: remove typoed -/'s in to_additive docstrings
5227886
@thorimur
feat: tfae block tactic
e3d1979
@thorimur
docs: tfae block tactic
090514a
@thorimur
test: tfae block tactic; clean up some unnecessary tests
80e8090
@thorimur
chore: revert tfae_have : to tfae_have
3f0b242
@thorimur
Merge remote-tracking branch 'origin/tfae-have-stx-tweak' into tfae-c…
a1cd0d0 
…hore-syntax-update
@thorimur
Merge branch 'lint-backarrow-fix' into tfae-block-tactic
e506660
@thorimur
lint: make tfaeFields parser private
3025412
@thorimur
thorimur force-pushed the tfae-block-syntax-update branch from b1b1784 to 5f37ef2 Compare September 13, 2024 01:03
@github-actions

github-actions Bot commented Sep 13, 2024 •
edited
Loading

Copy link
Copy Markdown

PR summary 36b056950a

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Tactic.TFAE 21 25 +4 (+19.05%)
Mathlib.CategoryTheory.Bicategory.Kan.Adjunction 440 441 +1 (+0.23%)
Mathlib.Order.WellFoundedSet 518 519 +1 (+0.19%)
Mathlib.Order.CompactlyGenerated.Basic 531 532 +1 (+0.19%)
Mathlib.Topology.LocallyClosed 560 561 +1 (+0.18%)
Mathlib.Topology.Inseparable 564 565 +1 (+0.18%)
Mathlib.Order.Height 590 591 +1 (+0.17%)
Mathlib.Topology.Separation 608 609 +1 (+0.16%)
Mathlib.Topology.UniformSpace.UniformConvergence 659 660 +1 (+0.15%)
Mathlib.Topology.NoetherianSpace 676 677 +1 (+0.15%)
Mathlib.Topology.LocallyConstant.Basic 677 678 +1 (+0.15%)
Mathlib.Topology.Order.LeftRightNhds 731 732 +1 (+0.14%)
Mathlib.SetTheory.Ordinal.Topology 768 769 +1 (+0.13%)
Mathlib.CategoryTheory.Abelian.Exact 835 836 +1 (+0.12%)
Mathlib.Algebra.Homology.ShortComplex.ExactFunctor 838 839 +1 (+0.12%)
Mathlib.Algebra.Exact 840 841 +1 (+0.12%)
Mathlib.Algebra.Order.ToIntervalMod 846 847 +1 (+0.12%)
Mathlib.Topology.Algebra.Group.SubmonoidClosure 886 887 +1 (+0.11%)
Mathlib.RingTheory.Valuation.Basic 894 895 +1 (+0.11%)
Mathlib.RingTheory.LocalRing.RingHom.Basic 900 901 +1 (+0.11%)
Mathlib.Analysis.BoxIntegral.Box.Basic 902 903 +1 (+0.11%)
Mathlib.RingTheory.Bezout 1020 1021 +1 (+0.10%)
Mathlib.NumberTheory.FLT.Basic 1024 1025 +1 (+0.10%)
Mathlib.RingTheory.Valuation.ValuationRing 1035 1036 +1 (+0.10%)
Mathlib.GroupTheory.Nilpotent 1127 1128 +1 (+0.09%)
Mathlib.RingTheory.Henselian 1213 1214 +1 (+0.08%)
Mathlib.Analysis.RCLike.Basic 1229 1230 +1 (+0.08%)
Mathlib.MeasureTheory.Group.Action 1239 1240 +1 (+0.08%)
Mathlib.Analysis.SpecificLimits.Normed 1258 1259 +1 (+0.08%)
Mathlib.RingTheory.DiscreteValuationRing.TFAE 1265 1266 +1 (+0.08%)
Mathlib.Analysis.LocallyConvex.WithSeminorms 1273 1274 +1 (+0.08%)
Mathlib.LinearAlgebra.Eigenspace.Zero 1278 1279 +1 (+0.08%)
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 1282 1283 +1 (+0.08%)
Mathlib.FieldTheory.Galois 1293 1294 +1 (+0.08%)
Mathlib.FieldTheory.KummerExtension 1322 1323 +1 (+0.08%)
Mathlib.Topology.Category.CompHaus.EffectiveEpi 1397 1398 +1 (+0.07%)
Mathlib.RingTheory.Flat.EquationalCriterion 1419 1420 +1 (+0.07%)
Mathlib.Topology.Category.Profinite.EffectiveEpi 1420 1421 +1 (+0.07%)
Mathlib.Topology.Category.Stonean.EffectiveEpi 1420 1421 +1 (+0.07%)
Mathlib.Analysis.InnerProductSpace.Basic 1586 1587 +1 (+0.06%)
Import changes for all files
Files Import difference
2391 files Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Analysis.Normed.Group.Uniform Mathlib.Data.Real.Hyperreal Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Topology.Algebra.Monoid Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Analysis.MeanInequalitiesPow Mathlib.Topology.Algebra.Module.Simple Mathlib.Algebra.Star.Module Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.RingTheory.IsAdjoinRoot Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Topology.Order.LawsonTopology Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.LinearAlgebra.FinsuppVectorSpace Mathlib.Probability.Process.HittingTime Mathlib.Data.Nat.Choose.Cast Mathlib.NumberTheory.Liouville.LiouvilleWith Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.RingTheory.Henselian Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.FieldTheory.IsPerfectClosure Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.RingTheory.HahnSeries.Basic Mathlib.Topology.Instances.Nat Mathlib.Algebra.Periodic Mathlib.CategoryTheory.Sites.Pullback Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.RingTheory.Polynomial.Content Mathlib.Topology.Algebra.Semigroup Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.Topology.CompactOpen Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerBasis Mathlib.Algebra.Symmetrized Mathlib.Algebra.Lie.Normalizer Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.FieldTheory.Finite.Trace Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.RingTheory.AlgebraTower Mathlib.Data.Matrix.Auto Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.Topology.IndicatorConstPointwise Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.ContinuousFunction.CompactlySupported Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.GroupTheory.Submonoid.Inverses Mathlib.Analysis.Convex.AmpleSet Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.RingTheory.Ideal.QuotientOperations Mathlib.Probability.Variance Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.RingTheory.SimpleModule Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Topology.MetricSpace.Thickening Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.LinearAlgebra.Finsupp Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Probability.Distributions.Geometric Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Subadditive Mathlib.NumberTheory.MulChar.Lemmas Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.Topology.Algebra.Order.Compact Mathlib.Algebra.Module.LocalizedModuleIntegers Mathlib.MeasureTheory.Integral.Marginal Mathlib.NumberTheory.Multiplicity Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.Topology.DerivedSet Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.LinearAlgebra.Projection Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Topology.Algebra.UniformField Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Algebra.Module.Bimodule Mathlib.Tactic.FunProp.ContDiff Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.LinearAlgebra.SModEq Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Algebra.Category.Grp.Subobject Mathlib.Analysis.Normed.Lp.PiLp Mathlib.LinearAlgebra.Span Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.RingTheory.WittVector.Domain Mathlib.Topology.Homotopy.Contractible Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Topology.DiscreteSubset Mathlib.Topology.Compactification.OnePoint Mathlib.RingTheory.Artinian Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Topology.Instances.PNat Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.FieldTheory.Laurent Mathlib.Analysis.Normed.Lp.WithLp Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Topology.DenseEmbedding Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.NumberTheory.GaussSum Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Lie.Quotient Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Condensed.Limits Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Topology.UniformSpace.Compact Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Topology.Order.Lattice Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.CategoryTheory.Abelian.Ext Mathlib.Topology.Sheaves.Sheaf Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Flat.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.RingTheory.HahnSeries.Addition Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Data.Real.GoldenRatio Mathlib.MeasureTheory.Order.Lattice Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.WittVector.InitTail Mathlib.Condensed.TopComparison Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Data.Finsupp.PWO Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Analysis.Hofer Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.LinearAlgebra.Dimension.Localization Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.LinearAlgebra.Lagrange Mathlib.ModelTheory.PartialEquiv Mathlib.RingTheory.AdicCompletion.Basic Mathlib.Data.Matrix.Invertible Mathlib.Topology.Instances.Int Mathlib.Analysis.Convex.Topology Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Complex Mathlib.Logic.Hydra Mathlib.LinearAlgebra.Coevaluation Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Algebra.Lie.Submodule Mathlib.FieldTheory.AbelRuffini Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Data.Matrix.Composition Mathlib.RingTheory.ClassGroup Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.RingTheory.Ideal.Maps Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Algebra.DirectSum.Module Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.GroupTheory.DoubleCoset Mathlib.Probability.StrongLaw Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Algebra.Category.Grp.AB5 Mathlib.Topology.Algebra.Ring.Basic Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.RingTheory.Regular.RegularSequence Mathlib.Topology.FiberBundle.Constructions Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.Data.Matrix.Basic Mathlib.Combinatorics.Hall.Basic Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.RingTheory.Derivation.Lie Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Data.ZMod.Module Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.Analysis.Complex.HalfPlane Mathlib.Data.Matrix.Basis Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.Topology.Sets.Closeds Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.MvPolynomial.Counit Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.Topology.Order.ScottTopology Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Algebra.MvPolynomial.Basic Mathlib.Analysis.Seminorm Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Analysis.Convex.Side Mathlib.NumberTheory.ArithmeticFunction Mathlib.MeasureTheory.Function.L2Space Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.Topology.VectorBundle.Hom Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Topology.Instances.CantorSet Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.RingTheory.Polynomial.Quotient Mathlib.Topology.ExtremallyDisconnected Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Topology.Category.TopCat.EpiMono Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.Topology.Bornology.BoundedOperation Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.ModularForms.Identities Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Algebra.MvPolynomial.Funext Mathlib.NumberTheory.NumberField.Norm Mathlib.Analysis.Convex.Body Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Analysis.NormedSpace.RCLike Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.DFinsupp Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Condensed.Light.Explicit Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Probability.CondCount Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Data.Real.Sqrt Mathlib.Topology.ContinuousFunction.Ideals Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.FieldTheory.Galois Mathlib.RingTheory.Trace.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.NumberTheory.LSeries.ZMod Mathlib.RingTheory.Bialgebra.Hom Mathlib.GroupTheory.OrderOfElement Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.CategoryTheory.Bicategory.Kan.Adjunction Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.NumberTheory.FLT.Four Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Probability.Distributions.Exponential Mathlib.Data.Matrix.PEquiv Mathlib.Algebra.RingQuot Mathlib.RingTheory.WittVector.MulCoeff Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.RingTheory.RingHom.FiniteType Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Germ Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.Algebra.Group.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Topology.ShrinkingLemma Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.RingTheory.Localization.BaseChange Mathlib.Algebra.Lie.Nilpotent Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.FieldTheory.Normal Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.Topology.CountableSeparatingOn Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.MeasureTheory.Group.Measure Mathlib.Topology.Order.ExtendFrom Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.Probability.Kernel.Composition Mathlib.NumberTheory.Liouville.LiouvilleNumber Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Algebra.Category.Grp.Abelian Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Dynamics.OmegaLimit Mathlib.RingTheory.Localization.Ideal Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.RingTheory.Polynomial.Opposites Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.GroupTheory.Perm.Closure Mathlib.RingTheory.Polynomial.Tower Mathlib.CategoryTheory.Sites.EpiMono Mathlib.GroupTheory.Abelianization Mathlib.Data.Finset.SMulAntidiagonal Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Probability.Martingale.Upcrossing Mathlib.Topology.Filter Mathlib.Topology.Order.PartialSups Mathlib.RingTheory.Coalgebra.Basic Mathlib.Topology.Algebra.SeparationQuotient Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.RingTheory.Jacobson Mathlib.Analysis.RCLike.Lemmas Mathlib.Algebra.Quaternion Mathlib.Condensed.Explicit Mathlib.NumberTheory.MulChar.Basic Mathlib.Data.Nat.Choose.Lucas Mathlib.Algebra.Polynomial.Splits Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Norm.Defs Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.RingTheory.Kaehler.Polynomial Mathlib.GroupTheory.Exponent Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.WittVector.Identities Mathlib.Condensed.Module Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Convex.GaugeRescale Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Adjoin Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.Discriminant Mathlib.GroupTheory.Solvable Mathlib.Algebra.Category.Grp.Kernels Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.RingTheory.Polynomial.Dickson Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Topology.Sheaves.Forget Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Algebra.MvPolynomial.Expand Mathlib.Analysis.Oscillation Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Topology.ContinuousFunction.ContinuousMapZero Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Algebra.DualQuaternion Mathlib.Condensed.Light.CartesianClosed Mathlib.RingTheory.Localization.Integral Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Algebra.Lie.Derivation.Killing Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.FieldTheory.SeparableClosure Mathlib.Analysis.Complex.Circle Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Data.ZMod.Quotient Mathlib.RingTheory.WittVector.Truncated Mathlib.Algebra.Exact Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.Data.DFinsupp.WellFounded Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.NumberTheory.RamificationInertia Mathlib.Data.Nat.Squarefree Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Topology.ContinuousFunction.Polynomial Mathlib.FieldTheory.ChevalleyWarning Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.RepresentationTheory.Rep Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Star.Subalgebra Mathlib.Topology.LocalAtTarget Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.Data.Finsupp.Weight Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Analysis.Fourier.ZMod Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.Topology.LocallyConstant.Basic Mathlib.GroupTheory.Divisible Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.CubicDiscriminant Mathlib.Topology.Order.ProjIcc Mathlib.RingTheory.PrincipalIdealDomain Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Topology.ContinuousFunction.CocompactMap Mathlib.RingTheory.Ideal.MinimalPrime Mathlib.GroupTheory.Nilpotent Mathlib.Topology.MetricSpace.Cauchy Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Topology.Order.Hom.Esakia Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.GroupTheory.CommutingProbability Mathlib.Algebra.Lie.Free Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Analysis.Complex.Basic Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.Analysis.Convex.Intrinsic Mathlib.Topology.MetricSpace.Lipschitz Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.NoncommPiCoprod Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.AlgebraicGeometry.Spec Mathlib.MeasureTheory.Category.MeasCat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Analysis.Calculus.TangentCone Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.RingTheory.RingHom.Finite Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.RingTheory.EssentialFiniteness Mathlib.Algebra.Order.ToIntervalMod Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Polynomial.Inductions Mathlib.LinearAlgebra.PerfectPairing Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Data.Nat.Periodic Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.FieldTheory.SeparableDegree Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Topology.Instances.Discrete Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.RingTheory.PowerSeries.Derivative Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Constructions.Pi Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Topology.Spectral.Hom Mathlib.CategoryTheory.Sites.InducedTopology Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.RingTheory.Ideal.Cotangent Mathlib.Topology.PartialHomeomorph Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.LinearAlgebra.QuotientPi Mathlib.Topology.ClopenBox Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.Noetherian Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Topology.Sheaves.LocalPredicate Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.GroupTheory.SchurZassenhaus Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.LinearAlgebra.Trace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.LinearAlgebra.FreeModule.PID Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Dynamics.Ergodic.Conservative Mathlib.Topology.UniformSpace.CompareReals Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Topology.Instances.AddCircle Mathlib.Topology.Sequences Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.Topology.ContinuousFunction.Algebra Mathlib.Analysis.Convex.Slope Mathlib.Topology.Order.Monotone Mathlib.Probability.Kernel.WithDensity Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Topology.Category.Profinite.AsLimit Mathlib.RingTheory.Ideal.Quotient Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.GroupTheory.Perm.Fin Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Topology.Order.Bounded Mathlib.Data.Matrix.CharP Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Localization.Away.Basic Mathlib.Topology.Homotopy.Path Mathlib.Topology.Algebra.Order.Field Mathlib.FieldTheory.Finite.Basic Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Algebra.Algebra.Operations Mathlib.Topology.Order.LowerUpperTopology Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Analysis.Calculus.Taylor Mathlib.Data.ZMod.Coprime Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Topology.CompletelyRegular Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.Data.Complex.Exponential Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Condensed.Basic Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Algebra.Polynomial.Taylor Mathlib.FieldTheory.IsSepClosed Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.Category.TopCat.Basic Mathlib.Algebra.Lie.Killing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Topology.Maps.Proper.Basic Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.Order.CompactlyGenerated.Intervals Mathlib.Condensed.Light.TopComparison Mathlib.Topology.MetricSpace.Dilation Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.GroupTheory.GroupAction.Period Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.NumberTheory.PellMatiyasevic Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Lie.Character Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.ContinuousFunction.StarOrdered Mathlib.Topology.Sober Mathlib.RingTheory.Presentation Mathlib.Analysis.LocallyConvex.Basic Mathlib.Topology.Separation Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Topology.ExtendFrom Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Algebra.Lie.DirectSum Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.Probability.Martingale.Basic Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.RingTheory.Coprime.Ideal Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Algebra.Squarefree.Basic Mathlib.Analysis.Normed.Module.Span Mathlib.Algebra.Polynomial.Expand Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.FieldTheory.Finite.Polynomial Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.Topology.MetricSpace.ProperSpace Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.MeasureTheory.Measure.Content Mathlib.LinearAlgebra.FiniteDimensional Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.FieldTheory.Extension Mathlib.Topology.Order.Filter Mathlib.LinearAlgebra.Orientation Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Topology.Homotopy.Basic Mathlib.Algebra.DirectSum.Internal Mathlib.Data.Matrix.Block Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.NumberTheory.LSeries.Basic Mathlib.RingTheory.Valuation.ValuationRing Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.SumFourSquares Mathlib.Topology.UrysohnsBounded Mathlib.Combinatorics.Configuration Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.AlgebraicGeometry.Properties Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Data.ZMod.IntUnitsPower Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.Sub Mathlib.Topology.Algebra.Star Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.Real Mathlib.RingTheory.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Topology.Metrizable.Urysohn Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.LinearAlgebra.Semisimple Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Algebra.Lie.Weights.Basic Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Data.Set.MulAntidiagonal Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Topology.Order.Basic Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Topology.Algebra.Equicontinuity Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.SetTheory.Ordinal.Topology Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.RingTheory.PiTensorProduct Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.RingTheory.Flat.Algebra Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.Topology.Instances.ENat Mathlib.Topology.Homeomorph Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.RingTheory.Coalgebra.Hom Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.NumberTheory.Rayleigh Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.Condensed.Solid Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Topology.List Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.RingTheory.LocalRing.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Probability.Kernel.IntegralCompProd Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.RingTheory.Localization.Submodule Mathlib.RingTheory.Radical Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.RingTheory.Localization.Integer Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.Normed.Group.Quotient Mathlib.Topology.Category.CompHaus.Basic Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.InnerProductSpace.Basic Mathlib.RingTheory.Generators Mathlib.RingTheory.Adjoin.Tower Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Data.Complex.Determinant Mathlib.Analysis.Complex.OperatorNorm Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.AlgebraicTopology.SingularSet Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.Analysis.PSeriesComplex Mathlib.RingTheory.PolynomialAlgebra Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.RingTheory.QuotientNilpotent Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Topology.Algebra.UniformMulAction Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Algebra.Polynomial.Mirror Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.Algebra.Algebra.Unitization Mathlib.Analysis.Convex.Integral Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Gluing Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Topology.LocallyClosed Mathlib.CategoryTheory.Preadditive.Mat Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.MeasureTheory.Measure.Trim Mathlib.RingTheory.Polynomial.Bernstein Mathlib.Analysis.Normed.Group.Completeness Mathlib.Topology.Sets.Order Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Algebra.LinearRecurrence Mathlib.MeasureTheory.Constructions.Prod.Integral Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Topology.Algebra.StarSubalgebra Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.GroupTheory.FiniteAbelian Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Topology.UniformSpace.Matrix Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.NumberTheory.PythagoreanTriples Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Topology.MetricSpace.Isometry Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.Algebra.MvPolynomial.Rename Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.Condensed.Light.Epi Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.Complex.ReImTopology Mathlib.RingTheory.ZMod Mathlib.Algebra.Polynomial.Monic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Data.Matrix.Reflection Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Algebra.Module.Projective Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.LinearAlgebra.CrossProduct Mathlib.Analysis.Complex.Schwarz Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.RingTheory.Adjoin.FG Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.CategoryTheory.Abelian.Injective Mathlib.Dynamics.Newton Mathlib.Topology.Hom.Open Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.Topology.Algebra.MulAction Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.LinearAlgebra.Basis.Defs Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Convex.Join Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.GroupTheory.QuotientGroup.Basic Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.PartitionOfUnity Mathlib.Algebra.Polynomial.Coeff Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.FieldTheory.MvPolynomial Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.Analysis.SumOverResidueClass Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.Algebra.MvPolynomial.Derivation Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.Topology.ContinuousFunction.Basic Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Data.Real.Pi.Leibniz Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.Algebra.MvPolynomial.Variables Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.Algebra.Order.Chebyshev Mathlib.RepresentationTheory.Basic Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.NumberTheory.FLT.Three Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.Filtration Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.SpecialFunctions.Polynomials Mathlib.Topology.MetricSpace.Polish Mathlib.RingTheory.Nakayama Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.GroupTheory.CosetCover Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Topology.MetricSpace.Infsep Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Topology.Category.Profinite.Basic Mathlib.CategoryTheory.Abelian.Projective Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Algebra.Lie.Weights.Chain Mathlib.MeasureTheory.Group.LIntegral Mathlib.Topology.Instances.Rat Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.RingTheory.Algebraic Mathlib.Topology.Algebra.ProperAction Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Algebra.Polynomial.Derivation Mathlib.Probability.Kernel.Invariance Mathlib.Topology.Order.NhdsSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.Topology.ContinuousFunction.Ordered Mathlib.Tactic.ComputeDegree Mathlib.Probability.Distributions.Uniform Mathlib.SetTheory.Surreal.Dyadic Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Geometry.Euclidean.Basic Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Algebra.MvPolynomial.Supported Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Geometry.RingedSpace.Basic Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Data.Matrix.Rank Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.Liouville.Measure Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.GroupTheory.Torsion Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.LinearAlgebra.Dimension.Basic Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.ContinuousFunction.Weierstrass Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.Topology.MetricSpace.Algebra Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Topology.Order.LeftRightLim Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Algebra.DirectSum.Finsupp Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.LinearAlgebra.LinearIndependent Mathlib.Geometry.Euclidean.MongePoint Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.Analysis.Convex.Between Mathlib.GroupTheory.FixedPointFree Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.MeasureTheory.Group.Pointwise Mathlib.Algebra.AlgebraicCard Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.NumberTheory.Ostrowski Mathlib.Data.Real.Irrational Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Algebra.Polynomial.Induction Mathlib.LinearAlgebra.Contraction Mathlib.MeasureTheory.Measure.Doubling Mathlib.Algebra.Algebra.Spectrum Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Topology.Order.MonotoneConvergence Mathlib.Analysis.MeanInequalities Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.FieldTheory.PrimitiveElement Mathlib.Algebra.Star.CHSH Mathlib.Probability.Distributions.Poisson Mathlib.RingTheory.Binomial Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.RingHom.Integral Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Condensed.TopCatAdjunction Mathlib.Algebra.Module.Submodule.Localization Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Topology.Algebra.MvPolynomial Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.InnerProductSpace.Projection Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.NormedSpace.MStructure Mathlib.Computability.TMComputable Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Data.ZMod.Basic Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.Topology.Algebra.UniformConvergence Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.RingTheory.SurjectiveOnStalks Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Analysis.Convex.Independent Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.RingTheory.ChainOfDivisors Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Topology.Algebra.ConstMulAction Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.Analysis.Complex.Asymptotics Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Probability.ConditionalProbability Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Topology.NoetherianSpace Mathlib.Order.Filter.ENNReal Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.CategoryTheory.Galois.Topology Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Algebra.Polynomial.Derivative Mathlib.Topology.Algebra.Field Mathlib.Data.Complex.FiniteDimensional Mathlib.Topology.ContinuousFunction.Units Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.Topology.Algebra.UniformRing Mathlib.RingTheory.OrzechProperty Mathlib.LinearAlgebra.Matrix.Trace Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Analysis.BoxIntegral.Basic Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.RingTheory.Polynomial.Basic Mathlib.Analysis.Quaternion Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Algebra.Lie.Abelian Mathlib.LinearAlgebra.SesquilinearForm Mathlib.Data.Matrix.Kronecker Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.RingTheory.HopfAlgebra Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Analysis.Normed.Group.Bounded Mathlib.Data.ZMod.Parity Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Topology.Category.TopCat.Opens Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.GroupTheory.Commensurable Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Algebra.Star.RingQuot Mathlib.CategoryTheory.CofilteredSystem Mathlib.RingTheory.Discriminant Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.NumberTheory.SumTwoSquares Mathlib.GroupTheory.Complement Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.DirectLimit Mathlib.MeasureTheory.Measure.VectorMeasure Mathlib.RingTheory.ReesAlgebra Mathlib.Analysis.Analytic.Meromorphic Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.Module.PID Mathlib.Algebra.MvPolynomial.Comap Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Analysis.Convex.KreinMilman Mathlib.RingTheory.Ideal.AssociatedPrime Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Topology.Covering Mathlib.RingTheory.Polynomial.Wronskian Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Analysis.NormedSpace.Extr Mathlib.NumberTheory.ClassNumber.Finite Mathlib.FieldTheory.Finiteness Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.UnitInterval Mathlib.Topology.UrysohnsLemma Mathlib.NumberTheory.Harmonic.Int Mathlib.Topology.Category.CompactlyGenerated Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.CategoryTheory.Sites.Spaces Mathlib.Algebra.Pointwise.Stabilizer Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.Algebra.Algebra.RestrictScalars Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.NumberTheory.MaricaSchoenheim Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Data.Real.StarOrdered Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.Analysis.Normed.Order.Basic Mathlib.Algebra.CharP.ExpChar Mathlib.Topology.Metrizable.Basic Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.MeasureTheory.Measure.Count Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.CategoryTheory.Galois.Full Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.LinearAlgebra.FreeAlgebra Mathlib.Analysis.Complex.RemovableSingularity Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.RingTheory.JacobsonIdeal Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Analysis.Convex.Normed Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Probability.Kernel.Basic Mathlib.GroupTheory.Index Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.GroupTheory.Perm.Finite Mathlib.Topology.Algebra.UniformGroup Mathlib.Topology.FiberBundle.Trivialization Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.Topology.Algebra.OpenSubgroup Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.MeasureTheory.Constructions.Prod.Basic Mathlib.Topology.Sheaves.Limits Mathlib.Analysis.Convex.EGauge Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.LinearAlgebra.Ray Mathlib.Topology.ContinuousFunction.Sigma Mathlib.CategoryTheory.Localization.Triangulated Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Convex.Mul Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.StoneCech Mathlib.CategoryTheory.Triangulated.Opposite Mathlib.Topology.Algebra.Polynomial Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Analysis.Convex.Segment Mathlib.Data.ZMod.Units Mathlib.Analysis.Calculus.Darboux Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.MeasureTheory.Function.Jacobian Mathlib.FieldTheory.Perfect Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.Algebra.Module.Injective Mathlib.Topology.FiberBundle.Basic Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.Topology.MetricSpace.Contracting Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Data.Complex.Cardinality Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.MeasureTheory.Function.LpOrder Mathlib.RingTheory.UniqueFactorizationDomain Mathlib.Data.Set.SMulAntidiagonal Mathlib.Analysis.Convex.Measure Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Probability.Moments Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Topology.Baire.BaireMeasurable Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.NumberTheory.Cyclotomic.PID Mathlib.Analysis.NormedSpace.Int Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.RCLike.Basic Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.Topology.Specialization Mathlib.GroupTheory.ArchimedeanDensely Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.Normed.Operator.Banach Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Algebra.Module.CharacterModule Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Topology.Algebra.Algebra Mathlib.NumberTheory.Dioph Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Algebra.Module.Torsion Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.Complex Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.RingTheory.HahnSeries.Valuation Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Analysis.Convex.Contractible Mathlib.Data.Finsupp.WellFounded Mathlib.RingTheory.EuclideanDomain Mathlib.AlgebraicGeometry.AffineScheme Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.CategoryTheory.Sites.Equivalence Mathlib.Analysis.Normed.Ring.Units Mathlib.NumberTheory.Liouville.Basic Mathlib.NumberTheory.Padics.RingHoms Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Data.ZMod.Factorial Mathlib.Topology.Algebra.Constructions Mathlib.Topology.UniformSpace.Cauchy Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.RingTheory.Valuation.Integers Mathlib.Topology.MetricSpace.Perfect Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Algebra.Category.Grp.Images Mathlib.Order.Height Mathlib.FieldTheory.Separable Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.Connected.PathConnected Mathlib.Analysis.Normed.Operator.WeakOperatorTopology Mathlib.Topology.Order.DenselyOrdered Mathlib.RingTheory.HahnSeries.Summable Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Algebra.Module.FinitePresentation Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.Limits Mathlib.Topology.UniformSpace.Separation Mathlib.RingTheory.EisensteinCriterion Mathlib.Algebra.Star.Free Mathlib.RingTheory.Int.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Analysis.NormedSpace.ENorm Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.Algebra.Polynomial.BigOperators Mathlib.Topology.Algebra.Affine Mathlib.Analysis.CStarAlgebra.Basic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.Topology.Algebra.PontryaginDual Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Analysis.Analytic.Constructions Mathlib.RingTheory.Localization.Basic Mathlib.Topology.MetricSpace.Holder Mathlib.GroupTheory.QuotientGroup.Finite Mathlib.Algebra.MvPolynomial.Monad Mathlib.MeasureTheory.Measure.Dirac Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Analysis.SpecificLimits.Normed Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Topology.Algebra.FilterBasis Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.ModelTheory.Order Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.LinearAlgebra.Alternating.Basic Mathlib.RingTheory.WittVector.Frobenius Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Order.WellFoundedSet Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.Topology.ContinuousFunction.LocallyConstant Mathlib.RingTheory.AlgebraicIndependent Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.RingTheory.Localization.NumDen Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Topology.SeparatedMap Mathlib.Dynamics.Minimal Mathlib.NumberTheory.Pell Mathlib.Topology.ContinuousFunction.BoundedCompactlySupported Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Probability.Process.Stopping Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Geometry.RingedSpace.Stalks Mathlib.Condensed.Light.Limits Mathlib.Topology.Order.LeftRightNhds Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.NumberTheory.Modular Mathlib.RingTheory.WittVector.Basic Mathlib.Algebra.Homology.TotalComplex Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Tactic.ReduceModChar Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.Algebra.Polynomial.Eval Mathlib.Topology.VectorBundle.Constructions Mathlib.GroupTheory.Transfer Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.Combinatorics.Hindman Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Topology.MetricSpace.PiNat Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.Algebra.Polynomial.Reverse Mathlib.Topology.Category.Profinite.Extend Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.RingTheory.Smooth.Kaehler Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.RepresentationTheory.FDRep Mathlib.Analysis.Normed.Group.Lemmas Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.Algebra.MvPolynomial.Equiv Mathlib.GroupTheory.Coxeter.Inversion Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Condensed.CartesianClosed Mathlib.RingTheory.Ideal.IsPrimary Mathlib.Analysis.Convex.Function Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.ODE.Gronwall Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.Topology.ContinuousFunction.Compact Mathlib.GroupTheory.Finiteness Mathlib.Analysis.Analytic.Composition Mathlib.FieldTheory.RatFunc.Defs Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.VectorBundle.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.RingTheory.Bezout Mathlib.Analysis.ConstantSpeed Mathlib.Order.BooleanGenerators Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Topology.Category.Stonean.Basic Mathlib.SetTheory.Surreal.Multiplication Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.Analysis.Calculus.Implicit Mathlib.RingTheory.Unramified.Basic Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.FieldTheory.NormalClosure Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Geometry.Manifold.IntegralCurve Mathlib.Analysis.SumIntegralComparisons Mathlib.GroupTheory.PresentedGroup Mathlib.Topology.Instances.EReal Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.LinearAlgebra.Reflection Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Data.Complex.Order Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Combinatorics.SetFamily.CauchyDavenport Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.GroupTheory.Sylow Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.Probability.Kernel.MeasureCompProd Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.Topology.Order.OrderClosed Mathlib.Analysis.NormedSpace.Extend Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Analysis.Asymptotics.Theta Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Topology.Sets.Compacts Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.RingTheory.LocalProperties Mathlib.Topology.MetricSpace.Gluing Mathlib.MeasureTheory.Function.Egorov Mathlib.Probability.Independence.Basic Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.Analysis.Fourier.FourierTransform Mathlib.RingTheory.MatrixAlgebra Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Analysis.Convex.Cone.Basic Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.Tactic.FunProp.Differentiable Mathlib.RingTheory.AdjoinRoot Mathlib.Topology.ContinuousFunction.ZeroAtInfty Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.RingTheory.Coalgebra.Equiv Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Homology.LocalCohomology Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.CategoryTheory.Abelian.Exact Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.RepresentationTheory.Action.Continuous Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.Idempotents Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Dynamics.Flow Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Algebra.CharP.Quotient Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Division Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.RingTheory.Complex Mathlib.Analysis.Convolution Mathlib.AlgebraicGeometry.Scheme Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.MeasureTheory.Covering.Vitali Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Topology.EMetricSpace.Paracompact Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.Data.Complex.Module Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.FieldTheory.KummerExtension Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.NumberTheory.LucasPrimality Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.Analytic.Uniqueness Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.Condensed.Light.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.AlgebraicGeometry.Gluing Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.Topology.Sheaves.Functors Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.Analysis.Convex.Jensen Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Topology.Instances.Irrational Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.ContinuousFunction.T0Sierpinski Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.CategoryTheory.Sites.DenseSubsite Mathlib.Topology.Algebra.Module.Determinant Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.Topology.Algebra.GroupCompletion Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Analysis.MellinInversion Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.LucasLehmer Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.RingTheory.RingHomProperties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Topology.Sheaves.Operations Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.Data.Real.Cardinality Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Topology.Category.Sequential Mathlib.GroupTheory.PushoutI Mathlib.Analysis.Convex.Strict Mathlib.RingTheory.Valuation.Quotient Mathlib.Algebra.Category.Ring.Constructions Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.LinearAlgebra.Dimension.Free Mathlib.Dynamics.Ergodic.Function Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.Algebra.CharP.Reduced Mathlib.Algebra.Lie.BaseChange Mathlib.Algebra.CharZero.Quotient Mathlib.Analysis.Normed.Module.Basic Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.LinearAlgebra.Isomorphisms Mathlib.Analysis.Complex.Convex Mathlib.Topology.Separation.NotNormal Mathlib.Topology.DiscreteQuotient Mathlib.Topology.Category.Locale Mathlib.NumberTheory.PrimeCounting Mathlib.Topology.UniformSpace.Pi Mathlib.LinearAlgebra.Dual Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.RingTheory.Valuation.ValExtension Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Normed.Group.Pointwise Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.ModelTheory.Fraisse Mathlib.LinearAlgebra.Matrix.Basis Mathlib.RingTheory.Bialgebra.Equiv Mathlib.Topology.Sets.Opens Mathlib.Algebra.Polynomial.Lifts Mathlib.RingTheory.Finiteness Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Covering.Differentiation Mathlib.GroupTheory.HNNExtension Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.Topology.Category.CompHausLike.Limits Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Topology.Instances.RealVectorSpace Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.Convex.Hull Mathlib.RingTheory.Fintype Mathlib.Analysis.Complex.Hadamard Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.RingTheory.Etale.Basic Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Analysis.Convex.Star Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Data.ZMod.Algebra Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.Algebra.Order.CompleteField Mathlib.Analysis.Analytic.CPolynomial Mathlib.RingTheory.Ideal.Norm Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Colon Mathlib.LinearAlgebra.Basis.Basic Mathlib.MeasureTheory.Measure.Restrict Mathlib.CategoryTheory.Triangulated.Functor Mathlib.Data.Finsupp.Lex Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.RingTheory.WittVector.Teichmuller Mathlib.NumberTheory.WellApproximable Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Convex.Basic Mathlib.Topology.LocallyConstant.Algebra Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.InformationTheory.Hamming Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Algebra.CharP.Algebra Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.RingTheory.Localization.Module Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Process.Adapted Mathlib.Algebra.Lie.Subalgebra Mathlib.RingTheory.MvPolynomial.Basic Mathlib.Analysis.Normed.Order.Lattice Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Topology.ContinuousFunction.Bounded Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Algebra.Lie.Sl2 Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Data.Nat.Factorial.Cast Mathlib.Analysis.Convex.Complex Mathlib.Data.Matrix.RowCol Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.PowerSeries.Order Mathlib.FieldTheory.PurelyInseparable Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Dynamics.FixedPoints.Topology Mathlib.Analysis.Normed.Module.Ray Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Analysis.Analytic.Within Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.CategoryTheory.Galois.Action Mathlib.Probability.Independence.Kernel Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.MeasureTheory.Group.Prod Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.Order.Category.Frm Mathlib.MeasureTheory.Integral.Pi Mathlib.Topology.Algebra.Localization Mathlib.Algebra.Algebra.Bilinear Mathlib.NumberTheory.NumberField.House Mathlib.Algebra.Category.Grp.Colimits Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Data.Matrix.DualNumber Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Algebra.Lie.Solvable Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Topology.Order.T5 Mathlib.Topology.KrullDimension Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Condensed.Epi Mathlib.GroupTheory.Coxeter.Length Mathlib.Algebra.Lie.Weights.Cartan Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.Probability.Process.Filtration Mathlib.LinearAlgebra.TensorPower Mathlib.RingTheory.Valuation.Minpoly Mathlib.Algebra.QuaternionBasis Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Basic Mathlib.NumberTheory.Bernoulli Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.LinearAlgebra.SymplecticGroup Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.Topology.Order.Priestley Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.CategoryTheory.Extensive Mathlib.NumberTheory.LSeries.Linearity Mathlib.Analysis.NormedSpace.Real Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Data.DFinsupp.Lex Mathlib.Topology.Perfect Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.LinearAlgebra.Dimension.StrongRankCondition Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Data.Matrix.Hadamard Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.ModelTheory.DirectLimit Mathlib.Algebra.Lie.Engel Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Topology.Sheaves.PUnit Mathlib.RingTheory.WittVector.Defs Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Algebra.Lie.Rank Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Probability.Kernel.Condexp Mathlib.Condensed.Light.Functors Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.Topology.Compactness.Paracompact Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.GroupTheory.Order.Min Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.Topology.Sheaves.Presheaf Mathlib.Analysis.Asymptotics.Asymptotics Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.CategoryTheory.Adhesive Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.MeasureTheory.Measure.WithDensity Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.MeasureTheory.Function.AEEqFun Mathlib.Algebra.Lie.Classical Mathlib.Algebra.CharP.Two Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.Data.Complex.Abs Mathlib.LinearAlgebra.PiTensorProduct Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Topology.Order.IntermediateValue Mathlib.NumberTheory.Liouville.Residual Mathlib.Topology.Algebra.Order.Floor Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.Algebra.Homology.Bifunctor Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Algebra.Polynomial.Bivariate Mathlib.Analysis.Analytic.Inverse Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Topology.IsLocalHomeomorph Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.Restrict Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Normed.Operator.Compact Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.RingTheory.MaximalSpectrum Mathlib.Topology.Algebra.Order.Rolle Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.RingTheory.Unramified.Derivations Mathlib.Probability.Distributions.Gamma Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.Algebra.Polynomial.Roots Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Analysis.Normed.Group.Constructions Mathlib.RingTheory.Ideal.Basic Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.RingTheory.FiniteType Mathlib.RingTheory.Ideal.Basis Mathlib.Condensed.Functors Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.MeasureTheory.Constructions.Projective Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Analysis.NormedSpace.BallAction Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Algebra.CharP.IntermediateField Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.NumberTheory.Padics.ProperSpace Mathlib.MeasureTheory.Group.Action Mathlib.Probability.Density Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.Topology.Category.TopCommRingCat Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.Condensed.Equivalence Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Calculus.Dslope Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Topology.Homotopy.Equiv Mathlib.FieldTheory.IntermediateField.Basic Mathlib.RingTheory.Ideal.Prod Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Analysis.NormedSpace.Connected Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Category.Profinite.Product Mathlib.RingTheory.IntegralDomain Mathlib.Topology.Homotopy.HSpaces Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Algebra.DirectSum.Algebra Mathlib.Topology.Connected.Separation Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.MetricSpace.Completion Mathlib.Analysis.ODE.PicardLindelof Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Topology.Category.UniformSpace Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.Topology.Instances.NNReal Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.RingTheory.Localization.Cardinality Mathlib.Topology.Order.ExtrClosure Mathlib.Probability.ConditionalExpectation Mathlib.Analysis.Calculus.LogDeriv Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.FieldTheory.Tower Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Topology.Category.FinTopCat Mathlib.NumberTheory.FLT.Basic Mathlib.Analysis.Analytic.Polynomial Mathlib.RingTheory.PrimeSpectrum Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Algebra.CharP.MixedCharZero Mathlib.GroupTheory.Frattini Mathlib.Algebra.Polynomial.Identities Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Algebra.CharP.CharAndCard Mathlib.Topology.Metrizable.Uniformity Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.MvPolynomial.Invertible Mathlib.GroupTheory.PGroup Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.RingTheory.RingHom.Surjective Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.Dimension.Finite Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.RingTheory.DedekindDomain.PID Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.RingTheory.FreeRing Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.FieldTheory.AxGrothendieck Mathlib.Analysis.Convex.StoneSeparation Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.MeasureTheory.Integral.Indicator Mathlib.Algebra.DualNumber Mathlib.Algebra.Module.LocalizedModule Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Algebra.Star.Unitary Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Topology.Order.Hom.Basic Mathlib.Topology.Order.IsLUB Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Topology.MetricSpace.Closeds Mathlib.LinearAlgebra.FiniteSpan Mathlib.MeasureTheory.Group.Integral Mathlib.Topology.ContinuousFunction.StoneWeierstrass Mathlib.LinearAlgebra.LinearPMap Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Analysis.Convex.Radon Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Lie.TensorProduct Mathlib.FieldTheory.SplittingField.Construction Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.LinearAlgebra.Prod Mathlib.Data.Finset.MulAntidiagonal Mathlib.Topology.Sheaves.Sheafify Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.FieldTheory.RatFunc.Basic Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Topology.Semicontinuous Mathlib.RingTheory.Support Mathlib.Algebra.Lie.Weights.Linear Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.RingTheory.Unramified.Finite Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.RepresentationTheory.Maschke Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.Analysis.SpecificLimits.Basic Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.MeasureTheory.Function.EssSup Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.NumberTheory.Bertrand Mathlib.RingTheory.Valuation.Basic Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.GroupTheory.Schreier Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.RingTheory.NormTrace Mathlib.MeasureTheory.Measure.Complex Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.Data.Matrix.Notation Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.TensorProduct.Basic Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Topology.Order.MonotoneContinuity Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Geometry.Manifold.Metrizable Mathlib.Topology.Algebra.Module.Cardinality Mathlib.RingTheory.Valuation.RankOne Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.MeasureTheory.Function.Floor Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.Algebra.Algebra.Tower Mathlib.LinearAlgebra.Basis.Flag Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Algebra.Ring.NegOnePow Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Lie.InvariantForm Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.Topology.AlexandrovDiscrete Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Topology.UniformSpace.Equiv Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.RingTheory.QuotientNoetherian Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Order.CompactlyGenerated.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Algebra.Polynomial.Module.AEval Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Topology.Sheaves.Stalks Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.Algebra.FreeAlgebra Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.Normed.Group.Hom Mathlib.RingTheory.PowerSeries.Trunc Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Algebra.ModEq Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.Normed.Group.Basic Mathlib.RingTheory.Perfection Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.RingTheory.Norm.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.FunctionField Mathlib.Algebra.DirectSum.LinearMap Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Probability.CDF Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.NumberTheory.DiophantineApproximation Mathlib.Data.Nat.Totient Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.MeasureTheory.Group.Defs Mathlib.Algebra.Polynomial.Smeval Mathlib.LinearAlgebra.StdBasis Mathlib.Analysis.Convex.Exposed Mathlib.RingTheory.Localization.Algebra Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.Dual Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.Analysis.Normed.Module.Completion Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Topology.Instances.Sign Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Topology.Instances.ENNReal Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.Probability.Martingale.Centering Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Algebra.Lie.OfAssociative Mathlib.Topology.Category.Stonean.Limits Mathlib.GroupTheory.FreeAbelianGroup Mathlib.RingTheory.PowerSeries.Inverse Mathlib.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.Topology.Inseparable Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Support Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Algebra.Polynomial.Div Mathlib.Topology.MetricSpace.Bounded Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Topology.QuasiSeparated Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.Quotient Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.Topology.Algebra.Order.Archimedean Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Data.Nat.Factorial.SuperFactorial
 1
Mathlib.Tactic.TFAE 4

Declarations diff

+ elabTFAEType
+ mkTFAEId
- mkImplType
- mkTFAEHypName
- tfaeHaveCore

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.

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 13, 2024
This was referenced Sep 13, 2024
Closed
Closed
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 16, 2024
mathlib-bors Bot pushed a commit that referenced this pull request Sep 20, 2024
@thorimur @urkud
feat: tfae_have ... := syntax (#10653)
6dcd0d9 
This PR refactors `tfae_have` in terms of `have`, thus supporting all the syntax that `have` supports. We can now also write:
```lean
example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry
  tfae_have 2 → 1
  | p => f p
  tfae_have ⟨mp, mpr⟩ : 2 ↔ 3 := sorry
  ...
```
Previously, `tfae_have` exclusively pushed a new goal to the top of the goal list, requiring that the result be proved via tactic.

This PR does not deprecate or remove the "old-style" syntax, but does de-document it. The removal of old-style syntax is done in #11000.

This tees us up for a `tfae` block tactic (#10991, #11003).

See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/tfae_have.201.20.E2.86.92.202.20.3A.3D.20syntax).



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@thorimur thorimur added the WIP Work in progress label Sep 20, 2024
@grunweg grunweg added the t-meta Tactics, attributes or user commands label May 3, 2025
@joneugster

joneugster commented Sep 19, 2026

Copy link
Copy Markdown
Contributor

Mathlib has moved to PRs from forks. This PR is still from a branch of the main repository and will soon be closed! Please migrate the content to a fork and reopen a PR from there if you wish to do so. See Zulip topic for more instructions. Thank you for contributing to mathlib!

@joneugster joneugster added the will-close-soon Unless something changes, we will close this PR soon label Sep 19, 2026
@joneugster joneugster mentioned this pull request Sep 19, 2026
Draft
@joneugster

joneugster commented Sep 19, 2026

Copy link
Copy Markdown
Contributor

I've linked this in #43967, I believe it will be simpler to recreate this PR from scratch if I do manage to adopt the block-tfae tactic, so I'm closing this here

@mathlib-dependent-issues mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 19, 2026
@mathlib-dependent-issues mathlib-dependent-issues Bot deleted a comment Sep 19, 2026
@mathlib-dependent-issues

mathlib-dependent-issues Bot commented Sep 19, 2026

Copy link
Copy Markdown

This PR/issue depends on:

@joneugster
joneugster marked this pull request as draft September 19, 2026 16:46
@mathlib-bors

mathlib-bors Bot commented Sep 19, 2026

Copy link
Copy Markdown
Contributor

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands will-close-soon Unless something changes, we will close this PR soon WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@thorimur @joneugster @kim-em @grunweg @YaelDillies @leanprover-community-bot-assistant @urkud