Skip to content

chore: lake shake --add-public --keep-implied --keep-prefix --fix - #43782

Open
mathlib-nolints[bot] wants to merge 2 commits into
masterfrom
shake
Open

chore: lake shake --add-public --keep-implied --keep-prefix --fix#43782
mathlib-nolints[bot] wants to merge 2 commits into
masterfrom
shake

Conversation

@mathlib-nolints

@mathlib-nolints mathlib-nolints Bot commented Sep 13, 2026

Copy link
Copy Markdown
Contributor

I am happy to shake some imports for you!

48 files changed · +52 imports added · -41 imports removed

workflow run for this PR
explain.txt

@mathlib-nolints @github-actions
chore: lake shake --add-public --keep-implied --keep-prefix --fix
bf32264 
48 files changed · +52 imports added · -41 imports removed
@github-actions

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

Copy link
Copy Markdown

PR summary 45755497a2

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Data.Matrix.Cartan 1807 1201 -606 (-33.54%)
Mathlib.Tactic.GCongr.CoreAttrs 139 93 -46 (-33.09%)
Mathlib.Data.Nat.Basic 170 161 -9 (-5.29%)
Mathlib.Topology.UniformSpace.Cauchy 860 815 -45 (-5.23%)
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Tactic 770 731 -39 (-5.06%)
Mathlib.Topology.UniformSpace.UniformConvergence 861 826 -35 (-4.07%)
Mathlib.Algebra.Regular.Pi 233 225 -8 (-3.43%)
Mathlib.Topology.Order.Cadlag 1466 1420 -46 (-3.14%)
Mathlib.Algebra.Regular.SMul 230 223 -7 (-3.04%)
Mathlib.Topology.UniformSpace.LocallyUniformConvergence 862 838 -24 (-2.78%)
Mathlib.Tactic.GRewrite 153 149 -4 (-2.61%)
Mathlib.Tactic.Inclusion.Core.DiscrTreeExt 94 93 -1 (-1.06%)
Mathlib.Tactic.Inclusion.Core.Extensions 96 95 -1 (-1.04%)
Mathlib.Tactic.Inclusion.Extension.Core.Init 97 96 -1 (-1.03%)
Mathlib.Tactic.CongrExclamation 110 109 -1 (-0.91%)
Mathlib.Algebra.Group.Equiv.TypeTags 224 222 -2 (-0.89%)
Mathlib.Data.Int.Basic 193 192 -1 (-0.52%)
Mathlib.Testing.Plausible.Sampleable 205 204 -1 (-0.49%)
Mathlib.Tactic.Inclusion.Core.Expr 275 274 -1 (-0.36%)
Mathlib.Tactic.Inclusion.Core.Inclusion 278 277 -1 (-0.36%)
Mathlib.Tactic.Inclusion.Core.Core 280 279 -1 (-0.36%)
Mathlib.Tactic.Inclusion.Core.Elab 281 280 -1 (-0.36%)
Mathlib.Tactic.Inclusion.ExtensionAPI.Basic 281 280 -1 (-0.36%)
Mathlib.Tactic.Inclusion.ExtensionAPI.Attr 282 281 -1 (-0.35%)
Mathlib.Tactic.Inclusion.Extension.Core.Core 284 283 -1 (-0.35%)
Mathlib.GroupTheory.Exponent 1131 1128 -3 (-0.27%)
Mathlib.Data.List.Basic 382 383 +1 (+0.26%)
Mathlib.GroupTheory.CommutingProbability 1431 1428 -3 (-0.21%)
Mathlib.MeasureTheory.Function.LpSeminorm.Count 2439 2435 -4 (-0.16%)
Mathlib.Topology.Compactness.NhdsKer 812 811 -1 (-0.12%)
Mathlib.Topology.DerivedSet 846 845 -1 (-0.12%)
Mathlib.Topology.CantorBendixson 958 957 -1 (-0.10%)
Mathlib.Topology.LocallyFinsupp 1033 1032 -1 (-0.10%)
Mathlib.LinearAlgebra.Eigenspace.Basic 1585 1584 -1 (-0.06%)
Mathlib.Analysis.Asymptotics.TVS 1670 1669 -1 (-0.06%)
Mathlib.NumberTheory.Padics.PadicNumbers 1701 1700 -1 (-0.06%)
Mathlib.Probability.Independence.Kernel.Indep 1780 1779 -1 (-0.06%)
Mathlib.Analysis.Complex.AbelLimit 1867 1866 -1 (-0.05%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary 2066 2065 -1 (-0.05%)
Mathlib.NumberTheory.Niven 2219 2218 -1 (-0.05%)
Import changes for all files
Files Import difference
Mathlib.Data.Matrix.Cartan -606
Mathlib.Tactic.GCongr.CoreAttrs Mathlib.Topology.Order.Cadlag -46
Mathlib.Topology.UniformSpace.Cauchy -45
Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Tactic -39
Mathlib.Topology.UniformSpace.UniformConvergence -35
Mathlib.Topology.UniformSpace.LocallyUniformConvergence Mathlib.Topology.UniformSpace.UniformApproximation -24
7 files Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Algebra.Ring.Nat Mathlib.Data.Char Mathlib.Data.Nat.Basic Mathlib.Data.Nat.Find
 -9
21 files Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.Prod Mathlib.Algebra.Module.RingHom Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.GrindInstances Mathlib.Algebra.Ring.Invertible Mathlib.Algebra.Ring.Opposite Mathlib.Data.Int.Cast.Basic Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Nat.PSub Mathlib.GroupTheory.GroupAction.Hom Mathlib.Tactic.NormNum.Result
 -8
49 files Mathlib.Algebra.GroupWithZero.Action.Regular Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Ring.Torsion Mathlib.Algebra.Ring.Units Mathlib.Analysis.Asymptotics.Basic Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Asymptotics.Prod Mathlib.Analysis.Calculus.TangentCone.Defs Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Indicator Mathlib.Analysis.Normed.Group.Real Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Analysis.Normed.Module.MStructure Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.Oscillation Mathlib.Data.Int.Cast.Prod Mathlib.InformationTheory.Hamming Mathlib.Order.Filter.ENNReal Mathlib.Topology.Category.Sequential Mathlib.Topology.Compactness.CountablyCompact Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.TransferInstance Mathlib.Topology.MetricSpace.Ultra.Pi Mathlib.Topology.Metrizable.Basic Mathlib.Topology.Metrizable.Real Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Sequences Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.UniformSpace.Real Mathlib.Topology.UniformSpace.Ultra.Constructions Mathlib.Topology.UniformSpace.UniformEmbedding
 -7
24 files Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Int Mathlib.RingTheory.MvPowerSeries.GaussNorm Mathlib.RingTheory.Polynomial.GaussNorm Mathlib.RingTheory.PowerSeries.GaussNorm Mathlib.Tactic.NormNum.Core Mathlib.Topology.Bornology.Real Mathlib.Topology.Category.UniformSpace Mathlib.Topology.GDelta.MetrizableSpace Mathlib.Topology.Instances.Int Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Topology.MetricSpace.Bounded Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Topology.UniformSpace.Equiv Mathlib.Topology.UniformSpace.HeineCantor Mathlib.Topology.UniformSpace.Ultra.Completion Mathlib.Topology.UniformSpace.UniformConvergenceTopology
 -6
4 files Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.BoxIntegral.Partition.Tagged
 -5
12 files Mathlib.MeasureTheory.Function.LpSeminorm.Count Mathlib.Tactic.ClickSuggestions.ApplyAt Mathlib.Tactic.ClickSuggestions.Apply Mathlib.Tactic.ClickSuggestions.FindPremises Mathlib.Tactic.ClickSuggestions.GRewrite Mathlib.Tactic.ClickSuggestions.Rewrite Mathlib.Tactic.ClickSuggestions.SectionState Mathlib.Tactic.ClickSuggestions.TryPremises Mathlib.Tactic.ClickSuggestions.Unfold Mathlib.Tactic.ClickSuggestions.Util Mathlib.Tactic.ClickSuggestions Mathlib.Tactic.GRewrite
 -4
3 files Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.GroupAction.Period
 -3
Mathlib.Algebra.Group.Equiv.TypeTags -2
2182 files Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.DirectSum.LinearMap Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Field.Basic Mathlib.Algebra.Field.ModEq Mathlib.Algebra.Field.ULift Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.Pi Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Embedding Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Pointwise.Set.SelfInv Mathlib.Algebra.Group.Pointwise.Set.Small Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.Defs Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.MulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.MulOpposite Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.Support Mathlib.Algebra.Group.TypeTags.Pointwise Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero Mathlib.Algebra.GroupWithZero.Submonoid.Instances Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Lie.AdjointAction.Basic Mathlib.Algebra.Lie.AdjointAction.JordanChevalley Mathlib.Algebra.Lie.Basis.Base Mathlib.Algebra.Lie.Basis.Basic Mathlib.Algebra.Lie.Basis.Prod Mathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.CartanCriterion Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Classical Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.SerreConstruction Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Algebra.Lie.Sl2 Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Algebra.Module.SpanRankOperations Mathlib.Algebra.Module.StablyFree.FreeOfInvertible Mathlib.Algebra.Module.Torsion.Basic Mathlib.Algebra.Module.Torsion.PrimaryComponent Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Module.ZLattice.Summable Mathlib.Algebra.Module.ZMod Mathlib.Algebra.Notation.Indicator Mathlib.Algebra.Notation.Support Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.Archimedean.Defs Mathlib.Algebra.Order.BigOperators.GroupWithZero.List Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.End Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Algebra.Order.Group.Action Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Algebra.Order.Group.Cyclic Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.End Mathlib.Algebra.Order.Group.Equiv Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Synonym Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Basic Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.GroupWithZero.Defs Mathlib.Algebra.Order.GroupWithZero.OrderIso Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.Order.Hom.Basic Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.Submonoid Mathlib.Algebra.Order.Hom.TypeTags Mathlib.Algebra.Order.Hom.Units Mathlib.Algebra.Order.Interval.Set.Group Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Algebra.Order.IsBotOne Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.Lex Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Units Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.Units Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Positive.Field Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Ring.Defs Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Order.Ring.Synonym Mathlib.Algebra.Order.Ring.Unbundled.Basic Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.Sum Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Algebra.QuadraticAlgebra.NormDeterminant Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.Idempotent Mathlib.Algebra.Ring.Int.Defs Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Submonoid.Basic Mathlib.Algebra.Ring.Subsemiring.Defs Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Star.LinearMap Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.Birational.Birational Mathlib.AlgebraicGeometry.Birational.Composition Mathlib.AlgebraicGeometry.Birational.Dominant Mathlib.AlgebraicGeometry.Birational.RationalMap Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.AlgebraicGeometry.Geometrically.Connected Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.FlatRank Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.OrderOfVanishing Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.Sites.AffineEtale Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.EtalePoint Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.Binomial Mathlib.Analysis.Analytic.CPolynomialDef Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.ConvergenceRadius Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.Order Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.WithLp Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.Commutative.PosPart Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Transfer Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.CStarAlgebra.Extreme Mathlib.Analysis.CStarAlgebra.Fuglede Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.PositiveLinearFunctional Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.Projection Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.Calculus.AbsolutelyMonotone Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Comp Mathlib.Analysis.Calculus.ContDiff.Convolution Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.Deriv Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.Operations Mathlib.Analysis.Calculus.ContDiff.Polynomial Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.RestrictScalars Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.CompMul Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.Calculus.Deriv.MeanValue Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DerivativeTest Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.DifferentialForm.Basic Mathlib.Analysis.Calculus.DifferentialForm.VectorField Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Affine Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.CompCLM Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Congr Mathlib.Analysis.Calculus.FDeriv.Const Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap Mathlib.Analysis.Calculus.FDeriv.Defs Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.OfCompLeft Mathlib.Analysis.Calculus.FDeriv.Partial Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Pow Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.ImplicitContDiff Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.IteratedDeriv.Analytic Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.LogDerivUniformlyOn Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.TaylorIntegral Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.BorelCaratheodory Mathlib.Analysis.Complex.BranchLogRoot Mathlib.Analysis.Complex.CanonicalDecomposition Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.CoveringMap Mathlib.Analysis.Complex.ExponentialBounds Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.Liouville Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.Harmonic.Poisson Mathlib.Analysis.Complex.HasPrimitives Mathlib.Analysis.Complex.Isometry Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.MeanValue Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Poisson Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.GaussLucas Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.RiemannMapping Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.SqrtDeriv Mathlib.Analysis.Complex.SummableUniformlyOn Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Measure Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.ValueDistribution.Cartan Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation Mathlib.Analysis.Convex.Approximation Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Cone.Dual Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.TensorProduct Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.ContDiffMapSupportedIn Mathlib.Analysis.Distribution.DerivNotation Mathlib.Analysis.Distribution.Distribution Mathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.SchwartzSpace.Basic Mathlib.Analysis.Distribution.SchwartzSpace.Deriv Mathlib.Analysis.Distribution.SchwartzSpace.Fourier Mathlib.Analysis.Distribution.Sobolev Mathlib.Analysis.Distribution.Support Mathlib.Analysis.Distribution.TemperateGrowth Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Distribution.TestFunction Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.BesselPotentialSpace Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Affine Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.CanonicalTensor Mathlib.Analysis.InnerProductSpace.Coalgebra Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Continuous Mathlib.Analysis.InnerProductSpace.Convex Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.ExteriorPower Mathlib.Analysis.InnerProductSpace.GramMatrix Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.Harmonic.Basic Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.Laplacian Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.MulOpposite Mathlib.Analysis.InnerProductSpace.NormDet Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection.Basic Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional Mathlib.Analysis.InnerProductSpace.Projection.Minimal Mathlib.Analysis.InnerProductSpace.Projection.Reflection Mathlib.Analysis.InnerProductSpace.Projection.Submodule Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Reproducing.Operations Mathlib.Analysis.InnerProductSpace.Reproducing Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.SingularValues Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.StandardSubspace Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TensorProduct Mathlib.Analysis.InnerProductSpace.Trace Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.AbsConvexOpen Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.HahnBanach Mathlib.Analysis.LocallyConvex.Montel Mathlib.Analysis.LocallyConvex.PointwiseConvergence Mathlib.Analysis.LocallyConvex.SeparatingDual Mathlib.Analysis.LocallyConvex.Separation Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.Matrix.Hermitian Mathlib.Analysis.Matrix.LDL Mathlib.Analysis.Matrix.Normed Mathlib.Analysis.Matrix.Order Mathlib.Analysis.Matrix.PosDef Mathlib.Analysis.Matrix.Spectrum Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Basic Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Meromorphic.Divisor Mathlib.Analysis.Meromorphic.FactorizedRational Mathlib.Analysis.Meromorphic.IsolatedZeros Mathlib.Analysis.Meromorphic.LogDeriv Mathlib.Analysis.Meromorphic.NormalForm Mathlib.Analysis.Meromorphic.Order Mathlib.Analysis.Meromorphic.RCLike Mathlib.Analysis.Meromorphic.TrailingCoefficient Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AsymptoticCone Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Affine.Convex Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.DualNumber Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.GelfandFormula Mathlib.Analysis.Normed.Algebra.GelfandMazur Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Field.Dense Mathlib.Analysis.Normed.Field.Krasner Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.Matrix Mathlib.Analysis.Normed.Lp.SmoothApprox Mathlib.Analysis.Normed.Lp.lpHolder Mathlib.Analysis.Normed.Module.Alternating.Basic Mathlib.Analysis.Normed.Module.Alternating.Curry Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin Mathlib.Analysis.Normed.Module.Bases Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.ContinuousInverse Mathlib.Analysis.Normed.Module.DoubleDual Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.HahnBanach Mathlib.Analysis.Normed.Module.Multilinear.Basic Mathlib.Analysis.Normed.Module.Multilinear.Curry Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.Normed.Module.RCLike.Basic Mathlib.Analysis.Normed.Module.RCLike.Extend Mathlib.Analysis.Normed.Module.RieszLemma Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Operator.Asymptotics Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.Basic Mathlib.Analysis.Normed.Operator.Bilinear Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative Mathlib.Analysis.Normed.Operator.CompleteCodomain Mathlib.Analysis.Normed.Operator.Completeness Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv Mathlib.Analysis.Normed.Operator.Extend Mathlib.Analysis.Normed.Operator.Fredholm.Basic Mathlib.Analysis.Normed.Operator.Fredholm.Open Mathlib.Analysis.Normed.Operator.Mul Mathlib.Analysis.Normed.Operator.NNNorm Mathlib.Analysis.Normed.Operator.NormedSpace Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite Mathlib.Analysis.Normed.Operator.Prod Mathlib.Analysis.Normed.Ring.InfiniteProd Mathlib.Analysis.Normed.Unbundled.SpectralNorm Mathlib.Analysis.ODE.Basic Mathlib.Analysis.ODE.ExistUnique Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.ODE.Transform Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Factorization Mathlib.Analysis.Polynomial.Fourier Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.BoundedContinuous Mathlib.Analysis.RCLike.ContinuousMap Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.Real.Pi.Bounds Mathlib.Analysis.Real.Pi.Chudnovsky Mathlib.Analysis.Real.Pi.Irrational Mathlib.Analysis.Real.Pi.Leibniz Mathlib.Analysis.Real.Pi.Wallis Mathlib.Analysis.SpecialFunctions.Arcosh Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Measurable Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.SpecialFunctions.FrullaniIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gamma.Digamma Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrability.Basic Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic Mathlib.Analysis.SpecialFunctions.Integrals.Basic Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.InvLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.Pochhammer Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric Mathlib.Analysis.SpecialFunctions.Sigmoid Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.SumIntegralExpDecay Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Basic.Countable.Small Mathlib.Basic.Logic.Lemmas Mathlib.Basic.Rel.Cover Mathlib.Basic.Rel.Separated Mathlib.Basic.Rel Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Enumerative.Pentagonal.EulerFunction Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Combinatorics.Quiver.Cast Mathlib.Combinatorics.Quiver.ConnectedComponent Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Weight Mathlib.Combinatorics.Quiver.Path Mathlib.Combinatorics.Quiver.SingleObj Mathlib.Combinatorics.Quiver.Symmetric Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Computability.AkraBazzi.SumTransform Mathlib.Control.EquivFunctor Mathlib.Control.Fix Mathlib.Data.Bool.Set Mathlib.Data.Bundle Mathlib.Data.Countable.Small Mathlib.Data.ENat.Basic Mathlib.Data.FP.Basic Mathlib.Data.FunLike.Graded Mathlib.Data.Int.Basic Mathlib.Data.Int.Cast.Field Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.NatAbs Mathlib.Data.Int.Range Mathlib.Data.List.DropRight Mathlib.Data.List.Find Mathlib.Data.List.Iterate Mathlib.Data.List.SplitLengths Mathlib.Data.List.TakeWhile Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Hyperoperation Mathlib.Data.Nat.Log Mathlib.Data.Nat.Order.Lemmas Mathlib.Data.Nat.Pairing Mathlib.Data.Nat.Set Mathlib.Data.Nat.Upto Mathlib.Data.Nat.WithBot Mathlib.Data.Ordmap.Ordnode Mathlib.Data.PEquiv Mathlib.Data.PFun Mathlib.Data.PNat.Defs Mathlib.Data.PNat.Equiv Mathlib.Data.PSigma.Order Mathlib.Data.Part Mathlib.Data.Prod.Lex Mathlib.Data.Rel.Cover Mathlib.Data.Rel.Separated Mathlib.Data.Rel Mathlib.Data.Semiquot Mathlib.Data.Set.Basic Mathlib.Data.Set.BoolIndicator Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.Disjoint Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Image Mathlib.Data.Set.Inclusion Mathlib.Data.Set.Insert Mathlib.Data.Set.Lattice.Bounded Mathlib.Data.Set.Lattice.Disjoint Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice.Indexed Mathlib.Data.Set.Lattice.Order Mathlib.Data.Set.Lattice Mathlib.Data.Set.List Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Order Mathlib.Data.Set.Pairwise.Basic Mathlib.Data.Set.Pairwise.Chain Mathlib.Data.Set.Pairwise.Lattice Mathlib.Data.Set.Piecewise Mathlib.Data.Set.Prod Mathlib.Data.Set.Restrict Mathlib.Data.Set.Sigma Mathlib.Data.Set.Subset Mathlib.Data.Set.Subsingleton Mathlib.Data.Set.SymmDiff Mathlib.Data.Set.UnionLift Mathlib.Data.SetLike.Basic Mathlib.Data.Setoid.Basic Mathlib.Data.Sigma.Order Mathlib.Data.Sum.Lattice Mathlib.Data.Sum.Order Mathlib.Data.ULift Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircleAdd Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Extreme Mathlib.Dynamics.Ergodic.RadonNikodym Mathlib.FieldTheory.AbelRuffini Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.AlgebraicClosure Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.CardinalEmb Mathlib.FieldTheory.Cardinality Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.Differential.Basic Mathlib.FieldTheory.Differential.Liouville Mathlib.FieldTheory.Finite.Basic Mathlib.FieldTheory.Finite.Extension Mathlib.FieldTheory.Finite.GaloisField Mathlib.FieldTheory.Finite.Polynomial Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Finite.Valuation Mathlib.FieldTheory.Galois.Abelian Mathlib.FieldTheory.Galois.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.Galois.NormalBasis Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.FieldTheory.IsPerfectClosure Mathlib.FieldTheory.IsSepClosed Mathlib.FieldTheory.Isaacs Mathlib.FieldTheory.JacobsonNoether Mathlib.FieldTheory.KrullTopology Mathlib.FieldTheory.KummerExtension Mathlib.FieldTheory.KummerPolynomial Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.FieldTheory.NormalizedTrace Mathlib.FieldTheory.PerfectClosure Mathlib.FieldTheory.Perfect Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.PrimitiveElement Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots Mathlib.FieldTheory.PurelyInseparable.Basic Mathlib.FieldTheory.PurelyInseparable.Exponent Mathlib.FieldTheory.PurelyInseparable.PerfectClosure Mathlib.FieldTheory.PurelyInseparable.Tower Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.RatFunc.IntermediateField Mathlib.FieldTheory.RatFunc.Luroth Mathlib.FieldTheory.RatFunc.Valuation Mathlib.FieldTheory.SeparableClosure Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.SeparablyGenerated Mathlib.FieldTheory.TranscendentalSeparable Mathlib.Geometry.Diffeology.Basic Mathlib.Geometry.Euclidean.Altitude Mathlib.Geometry.Euclidean.Angle.Bisector Mathlib.Geometry.Euclidean.Angle.Incenter Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.Projection Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.BritishFlag Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Incenter Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.NinePointCircle Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Projection Mathlib.Geometry.Euclidean.SignedDist Mathlib.Geometry.Euclidean.Similarity Mathlib.Geometry.Euclidean.Simplex Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.OrthRadius Mathlib.Geometry.Euclidean.Sphere.PolePolar Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Sphere.Tangent Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Euclidean.Volume.Measure Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.SMul Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.Bordism Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Category.MfldCat.OfModel Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.ContMDiff.Constructions Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.GroupLieAlgebra Mathlib.Geometry.Manifold.HasGroupoid Mathlib.Geometry.Manifold.ImmersionDiff Mathlib.Geometry.Manifold.Immersion Mathlib.Geometry.Manifold.Instances.Icc Mathlib.Geometry.Manifold.Instances.Quotient Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Geometry.Manifold.IsManifold.Basic Mathlib.Geometry.Manifold.IsManifold.ExtChartAt Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Geometry.Manifold.LocalSourceTargetProperty Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.Notation Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Riemannian.Basic Mathlib.Geometry.Manifold.Riemannian.PathELength Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.SmoothApprox Mathlib.Geometry.Manifold.SmoothEmbedding Mathlib.Geometry.Manifold.StructureGroupoid Mathlib.Geometry.Manifold.Submersion Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.LocalFrame Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.Riemannian Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.VectorBundle.Tensoriality Mathlib.Geometry.Manifold.VectorField.LieBracket Mathlib.Geometry.Manifold.VectorField.Pullback Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.GroupTheory.ArchimedeanDensely Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.GroupTheory.Descent Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.FinitelyPresentedGroup Mathlib.GroupTheory.Focal Mathlib.GroupTheory.Frattini Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.IsPerfect Mathlib.GroupTheory.Nilpotent Mathlib.GroupTheory.OreLocalization.OreSet Mathlib.GroupTheory.PGroup Mathlib.GroupTheory.Presentation Mathlib.GroupTheory.RegularWreathProduct Mathlib.GroupTheory.Schreier Mathlib.GroupTheory.SchurZassenhaus Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour Mathlib.GroupTheory.SpecificGroups.Alternating.Simple Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.GroupTheory.SpecificGroups.VirtuallyCyclic Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Subsemigroup.Center Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.GroupTheory.Subsemigroup.Lemmas Mathlib.GroupTheory.Sylow Mathlib.GroupTheory.Torsion Mathlib.GroupTheory.Transfer Mathlib.InformationTheory.Coding.PrefixFree Mathlib.InformationTheory.KullbackLeibler.Basic Mathlib.InformationTheory.KullbackLeibler.ChainRule Mathlib.InformationTheory.KullbackLeibler.DataProcessing Mathlib.InformationTheory.KullbackLeibler.KLFun Mathlib.LinearAlgebra.Center Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Complex.Determinant Mathlib.LinearAlgebra.Complex.Orientation Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.LinearAlgebra.Dual.BaseChange Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.LinearAlgebra.Eigenspace.Charpoly Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.LinearAlgebra.ExteriorAlgebra.Basis Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.LinearAlgebra.ExteriorAlgebra.Product Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.LinearAlgebra.ExteriorPower.Basis Mathlib.LinearAlgebra.ExteriorPower.BilinForm Mathlib.LinearAlgebra.ExteriorPower.Pairing Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient Mathlib.LinearAlgebra.FreeModule.ModN Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.LinearAlgebra.Matrix.Cartan.Basic Mathlib.LinearAlgebra.Matrix.Cartan.Realisation Mathlib.LinearAlgebra.Matrix.Cartan Mathlib.LinearAlgebra.Matrix.Charpoly.Disc Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.LinearAlgebra.Matrix.ElementaryRowOperations Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Matrix.Stochastic Mathlib.LinearAlgebra.Matrix.Swap Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.LinearAlgebra.Matrix.WithConv Mathlib.LinearAlgebra.Matrix.ZMatrix Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.Projectivization.Action Mathlib.LinearAlgebra.Projectivization.PSL.PSL2 Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer Mathlib.LinearAlgebra.QuadraticForm.AlgClosed Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.LinearAlgebra.QuadraticForm.Radical Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.LinearAlgebra.QuadraticForm.Signature Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.Reflection Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.LinearAlgebra.Semisimple Mathlib.LinearAlgebra.SesquilinearForm.Star Mathlib.LinearAlgebra.SpecialLinearGroup Mathlib.LinearAlgebra.Transvection.Basic Mathlib.LinearAlgebra.Transvection.Generation Mathlib.LinearAlgebra.Transvection Mathlib.LinearAlgebra.Unimodular Mathlib.Logic.Embedding.Basic Mathlib.Logic.Embedding.Set Mathlib.Logic.Equiv.Basic Mathlib.Logic.Equiv.Bool Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Equiv.Nat Mathlib.Logic.Equiv.Option Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Set Mathlib.Logic.Equiv.Sigma Mathlib.Logic.Function.Const Mathlib.Logic.Function.DependsOn Mathlib.Logic.Function.FiberPartition Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Set Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.AbsolutelyContinuous Mathlib.MeasureTheory.Function.BorelGrowth Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.ConditionalLExpectation Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.ConvergenceInDistribution Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.FactorsThrough Mathlib.MeasureTheory.Function.Holder Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.JacobianOneDim Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm Mathlib.MeasureTheory.Function.LpSpace.Basic Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp Mathlib.MeasureTheory.Function.LpSpace.Complete Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.LpSpace.Indicator Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.IntegralConvolution Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Group.ModularCharacter Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner.Basic Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus Mathlib.MeasureTheory.Integral.Bochner.L1 Mathlib.MeasureTheory.Integral.Bochner.Set Mathlib.MeasureTheory.Integral.Bochner.SumMeasure Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CircleAverage Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.CompactlySupported Mathlib.MeasureTheory.Integral.CurveIntegral.Basic Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FinMeasAdditive Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.MeanValue Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.Regular Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real Mathlib.MeasureTheory.Integral.SetToL1.ChangeMeasure Mathlib.MeasureTheory.Integral.SetToL1.DominatedConvergence Mathlib.MeasureTheory.Integral.SetToL1.Function Mathlib.MeasureTheory.Integral.SetToL1.L1 Mathlib.MeasureTheory.Integral.SetToL1.SimpleFunc Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion Mathlib.MeasureTheory.Measure.CharacteristicFunction Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasureExt Mathlib.MeasureTheory.Measure.FiniteMeasurePi Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.DistribChar Mathlib.MeasureTheory.Measure.Haar.Extension Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.MeasureTheory.Measure.IntegralCharFun Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyConvergence Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Prokhorov Mathlib.MeasureTheory.Measure.ResolventTransform Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.TightNormed Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap Mathlib.MeasureTheory.SpecificCodomains.Pi Mathlib.MeasureTheory.SpecificCodomains.WithLp Mathlib.MeasureTheory.VectorMeasure.AddContent Mathlib.MeasureTheory.VectorMeasure.BoundedVariation Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym Mathlib.MeasureTheory.VectorMeasure.Integral Mathlib.MeasureTheory.VectorMeasure.IntegrationByParts Mathlib.MeasureTheory.VectorMeasure.Prod Mathlib.MeasureTheory.VectorMeasure.SetIntegral Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation Mathlib.MeasureTheory.VectorMeasure.WithDensityVec Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.ArithmeticFunction.Carmichael Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.CarmichaelNumber Mathlib.NumberTheory.Chebyshev Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.FermatPsp Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Height.EllipticCurve Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZetaLogDeriv Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.NumberTheory.LegendreSymbol.Complex Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LocalField.Basic Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.LucasPrimality Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.BoundedAtCusp Mathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.NumberTheory.ModularForms.CuspFormSubmodule Mathlib.NumberTheory.ModularForms.Cusps Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.NumberTheory.ModularForms.Identities Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LFunction Mathlib.NumberTheory.ModularForms.LevelOne.Basic Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.ModularForms.RamanujanFormula Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.NumberTheory.Modular Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.MulChar.Lemmas Mathlib.NumberTheory.Niven Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Completion.InfinitePlace Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances Mathlib.NumberTheory.NumberField.Completion.Ramification Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.DirichletDensity Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.ExistsRamified Mathlib.NumberTheory.NumberField.FiniteAdeleRing Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.InfinitePlace.Basic Mathlib.NumberTheory.NumberField.InfinitePlace.Completion Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.Complex Mathlib.NumberTheory.Padics.HeightOneSpectrum Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.LocalField Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.Measure.AmiceTransform Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.Padics.ValuativeRel Mathlib.NumberTheory.Padics.WithVal Mathlib.NumberTheory.PowModTotient Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.NumberTheory.RamificationInertia.Inertia Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.NumberTheory.RamificationInertia.Valuation Mathlib.NumberTheory.RatFunc.Ostrowski Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SumFourSquares Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.SumTwoSquares Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.Wilson Mathlib.NumberTheory.ZetaValues Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.Order.Antichain Mathlib.Order.Antisymmetrization Mathlib.Order.Basic Mathlib.Order.BooleanAlgebra.Basic Mathlib.Order.BooleanAlgebra.Defs Mathlib.Order.BooleanAlgebra.Set Mathlib.Order.Booleanisation Mathlib.Order.BoundedOrder.Basic Mathlib.Order.BoundedOrder.Lattice Mathlib.Order.BoundedOrder.Monotone Mathlib.Order.Bounded Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Circular Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.Comparable Mathlib.Order.Compare Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Chain Mathlib.Order.CompleteLattice.Defs Mathlib.Order.CompleteLattice.Group Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.ConditionallyCompletePartialOrder.Basic Mathlib.Order.ConditionallyCompletePartialOrder.Defs Mathlib.Order.ConditionallyCompletePartialOrder.Indexed Mathlib.Order.Copy Mathlib.Order.Directed Mathlib.Order.Disjoint Mathlib.Order.Extension.Linear Mathlib.Order.Filter.AtTopBot.Basic Mathlib.Order.Filter.AtTopBot.CompleteLattice Mathlib.Order.Filter.AtTopBot.Defs Mathlib.Order.Filter.AtTopBot.Disjoint Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Map Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.Order.Filter.AtTopBot.Ring Mathlib.Order.Filter.AtTopBot.Tendsto Mathlib.Order.Filter.Bases.Basic Mathlib.Order.Filter.Basic Mathlib.Order.Filter.Curry Mathlib.Order.Filter.Defs Mathlib.Order.Filter.Ker Mathlib.Order.Filter.Lift Mathlib.Order.Filter.Map Mathlib.Order.Filter.NAry Mathlib.Order.Filter.Partial Mathlib.Order.Filter.Prod Mathlib.Order.Filter.SmallSets Mathlib.Order.Filter.Tendsto Mathlib.Order.GaloisConnection.Basic Mathlib.Order.GaloisConnection.Defs Mathlib.Order.Heyting.Basic Mathlib.Order.Heyting.Hom Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.Basic Mathlib.Order.Hom.BoundedLattice Mathlib.Order.Hom.Bounded Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Lattice Mathlib.Order.Hom.Lex Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.Hom.WithTopBot Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Lex Mathlib.Order.Interval.Set.Basic Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.LinearOrder Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Interval.Set.WithBotTop Mathlib.Order.Iterate Mathlib.Order.Lattice.Congruence Mathlib.Order.LatticeIntervals Mathlib.Order.Lattice Mathlib.Order.Max Mathlib.Order.MinMax Mathlib.Order.Minimal Mathlib.Order.Monotone.Basic Mathlib.Order.Monotone.Defs Mathlib.Order.Monotone.Extension Mathlib.Order.Monotone.Monovary Mathlib.Order.Monotone.Odd Mathlib.Order.Monotone.Union Mathlib.Order.Nat Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.OrderDual Mathlib.Order.Preorder.Chain Mathlib.Order.Prod.Lex.Hom Mathlib.Order.PropInstances Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelClasses Mathlib.Order.RelIso.Basic Mathlib.Order.RelIso.Set Mathlib.Order.ScottContinuity.Complete Mathlib.Order.ScottContinuity.Prod Mathlib.Order.ScottContinuity Mathlib.Order.SemiconjSup Mathlib.Order.SetIsMax Mathlib.Order.Set Mathlib.Order.SymmDiff Mathlib.Order.Types.Defs Mathlib.Order.ULift Mathlib.Order.UpperLower.Relative Mathlib.Order.WellFounded Mathlib.Order.WithBotTop Mathlib.Order.WithBot Mathlib.Order.Zorn Mathlib.Probability.BorelCantelli Mathlib.Probability.BrownianMotion.Basic Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily Mathlib.Probability.CDF Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.CramerWold Mathlib.Probability.Decision.BayesEstimator Mathlib.Probability.Density Mathlib.Probability.Distributions.Bernoulli Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Binomial Mathlib.Probability.Distributions.Cauchy Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Fernique Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson.Basic Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.Distributions.SetBernoulli Mathlib.Probability.Distributions.TwoValued Mathlib.Probability.Distributions.Uniform Mathlib.Probability.HasCondDistrib Mathlib.Probability.HasLawExists Mathlib.Probability.HasLaw Mathlib.Probability.IdentDistribIndep Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.BoundedContinuousFunction Mathlib.Probability.Independence.CharacteristicFunction Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.InfinitePi Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.Integration Mathlib.Probability.Independence.Kernel.IndepFun Mathlib.Probability.Independence.Kernel.Indep Mathlib.Probability.Independence.Process.Basic Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess Mathlib.Probability.Independence.Process.HasIndepIncrements Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Kernel.CompProdEqIff Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.RadonNikodym Mathlib.Probability.Kernel.Composition.WithDensity Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.IonescuTulcea.Traj Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.Posterior Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.Representation Mathlib.Probability.Kernel.SetIntegral Mathlib.Probability.Kernel.WithDensity Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.CovarianceBilinDual Mathlib.Probability.Moments.CovarianceBilin Mathlib.Probability.Moments.Covariance Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted Mathlib.Probability.Moments.Variance Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.FiniteDimensionalLaws Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.LocalProperty Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Predictable Mathlib.Probability.Process.Stopping Mathlib.Probability.ProductMeasure Mathlib.Probability.StrongLaw Mathlib.RepresentationTheory.AlgebraRepresentation.Basic Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.TateCohomology.Basic Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Irreducible Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.AdicCompletion.Completeness Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.RingTheory.AdicCompletion.LocalRing Mathlib.RingTheory.AdicCompletion.Noetherian Mathlib.RingTheory.AdicCompletion.RingHom Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.RingTheory.Complex Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Depth.Rees Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Discriminant Mathlib.RingTheory.DividedPowers.Padic Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Descent Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Finite Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.Etale.Weakly Mathlib.RingTheory.Extension.Basic Mathlib.RingTheory.Extension.Cotangent.BaseChange Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Extension.ExtendScalars Mathlib.RingTheory.Extension.Generators Mathlib.RingTheory.Extension.Presentation.Basic Mathlib.RingTheory.Extension.Presentation.Core Mathlib.RingTheory.Extension.Presentation.Submersive Mathlib.RingTheory.Flat.LocallyFree Mathlib.RingTheory.Flat.Rank Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.HopkinsLevitzki Mathlib.RingTheory.Ideal.CotangentBaseChange Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.KrullsHeightTheorem Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients.Basic Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients.Norm Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients Mathlib.RingTheory.Ideal.UFD Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralDomain Mathlib.RingTheory.Invariant.Galois Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Etale Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.LocalRing.ResidueField.Separable Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.MvPolynomial.Expand Mathlib.RingTheory.MvPowerSeries.Equiv Mathlib.RingTheory.MvPowerSeries.Expand Mathlib.RingTheory.Nilpotent.GeometricallyReduced Mathlib.RingTheory.NonUnitalSubsemiring.Defs Mathlib.RingTheory.Norm.Basic Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Norm.Transitivity Mathlib.RingTheory.NormTrace Mathlib.RingTheory.NormalClosure Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OrderOfVanishing.Basic Mathlib.RingTheory.OrderOfVanishing.Noetherian Mathlib.RingTheory.OreLocalization.OreSet Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.BDeRham Mathlib.RingTheory.Perfectoid.FontaineTheta Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.DegreeLT Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.Polynomial.Resultant.Basic Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.PowerSeries.Expand Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.QuasiFinite.Polynomial Mathlib.RingTheory.QuasiFinite.Weakly Mathlib.RingTheory.RamificationInertia.Basic Mathlib.RingTheory.RamificationInertia.Inertia Mathlib.RingTheory.RamificationInertia.Ramification Mathlib.RingTheory.Regular.Flat Mathlib.RingTheory.Regular.Free Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.Regular.LinearMap Mathlib.RingTheory.Regular.ProjectiveDimension Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RegularLocalRing.Polynomial Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.PurelyInseparable Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RingInvo Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.SimpleModule.IsAlgClosed Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.Quotient Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity Mathlib.RingTheory.Spectrum.Prime.Chevalley Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Spectrum.Prime.Homeomorph Mathlib.RingTheory.Spectrum.Prime.LTSeries Mathlib.RingTheory.Spectrum.Prime.Polynomial Mathlib.RingTheory.Teichmuller Mathlib.RingTheory.TensorProduct.IsBaseChangeHom Mathlib.RingTheory.TotallySplit Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Dedekind Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.LocalStructure Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.Archimedean Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing Mathlib.RingTheory.Valuation.Discrete.RankOne Mathlib.RingTheory.Valuation.DiscreteValuativeRel Mathlib.RingTheory.Valuation.FiniteField Mathlib.RingTheory.WittVector.Basic Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Complete Mathlib.RingTheory.WittVector.Defs Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.WittVector.Identities Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.WittVector.Isocrystal Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.WittVector.MulP Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.WittVector.TeichmullerSeries Mathlib.RingTheory.WittVector.Teichmuller Mathlib.RingTheory.WittVector.Truncated Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.ZMod.Torsion Mathlib.RingTheory.ZMod.UnitsCyclic Mathlib.RingTheory.ZariskisMainTheorem Mathlib.SetTheory.Cardinal.Defs Mathlib.SetTheory.Lists Mathlib.SetTheory.ZFC.PSet Mathlib.Tactic.ApplyFun Mathlib.Tactic.CancelDenoms.Core Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming Mathlib.Tactic.CongrExclamation Mathlib.Tactic.Convert Mathlib.Tactic.DeriveCountable Mathlib.Tactic.Inclusion.Core.Core Mathlib.Tactic.Inclusion.Core.DiscrTreeExt Mathlib.Tactic.Inclusion.Core.Elab Mathlib.Tactic.Inclusion.Core.Expr Mathlib.Tactic.Inclusion.Core.Extensions Mathlib.Tactic.Inclusion.Core.Inclusion Mathlib.Tactic.Inclusion.Core.ToSet Mathlib.Tactic.Inclusion.Extension.Core.Core Mathlib.Tactic.Inclusion.Extension.Core.Init Mathlib.Tactic.Inclusion.Extension.Interval Mathlib.Tactic.Inclusion.ExtensionAPI.Attr Mathlib.Tactic.Inclusion.ExtensionAPI.Basic Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic.Order.CollectFacts Mathlib.Tactic.Order.Graph.Basic Mathlib.Tactic.Order.Graph.Tarjan Mathlib.Tactic.Order.Preprocessing Mathlib.Tactic.Order.ToInt Mathlib.Tactic.Order Mathlib.Tactic.Peel Mathlib.Tactic.TautoSet Mathlib.Tactic.Zify Mathlib.Testing.Plausible.Sampleable Mathlib.Topology.AlexandrovDiscrete Mathlib.Topology.Algebra.Group.Matrix Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.TopDualPairing Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.Algebra.Star.LinearMap Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.WithVal Mathlib.Topology.Algebra.Valued.WithZeroMulInt Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.CantorBendixson Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Compactification.OnePoint.ProjectiveLine Mathlib.Topology.Compactification.OnePoint.Sphere Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.Compactness.NhdsKer Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.LocallyPathConnected Mathlib.Topology.Connected.PathComponentOne Mathlib.Topology.ContinuousMap.Bounded.Normed Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.ContinuousSqrt Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.LocallyConvex Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.Defs.Filter Mathlib.Topology.Defs.Sequences Mathlib.Topology.DerivedSet Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.LocallyContractible Mathlib.Topology.LocallyFinsupp.Pushforward Mathlib.Topology.LocallyFinsupp Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.Topology.MetricSpace.Congruence Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.Lipschitz Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.MetricSpace.ProperSpace.Real Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.MetricSpace.Similarity Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.Topology.MetricSpace.UniformConvergence Mathlib.Topology.Metrizable.CompletelyMetrizable Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.OmegaCompletePartialOrder Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Order.LawsonTopology Mathlib.Topology.Order.ScottTopology Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Topology.Semicontinuity.Hemicontinuity Mathlib.Topology.Semicontinuity.Michael Mathlib.Topology.Separation.AlexandrovDiscrete Mathlib.Topology.Separation.LinearUpperLowerSetTopology Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Specialization Mathlib.Topology.TietzeExtension Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.UniformSpace.Closeds Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.ContinuousAlternatingMap Mathlib.Topology.VectorBundle.FiniteDimensional Mathlib.Topology.VectorBundle.Hom Mathlib.Topology.VectorBundle.Riemannian
 -1
236 files Mathlib.Algebra.BigOperators.Group.Multiset.Defs Mathlib.Algebra.Category.MonCat.Limits Mathlib.Algebra.Category.MonCat.Shrink Mathlib.Algebra.CharZero.Infinite Mathlib.Algebra.FiniteSupport.Defs Mathlib.Algebra.FreeMonoid.Basic Mathlib.Algebra.FreeMonoid.Count Mathlib.Algebra.FreeMonoid.FreeSemigroup Mathlib.Algebra.FreeMonoid.Symbols Mathlib.Algebra.Group.Action.Pointwise.Set.Finite Mathlib.Algebra.Group.Action.TransferInstance Mathlib.Algebra.Group.Equiv.Finite Mathlib.Algebra.Group.Finsupp Mathlib.Algebra.Group.Nat.Range Mathlib.Algebra.Group.Shrink Mathlib.Algebra.Group.Submonoid.Finite Mathlib.Algebra.Group.Submonoid.Membership Mathlib.Algebra.Group.TransferInstance Mathlib.Algebra.Group.TypeTags.Finite Mathlib.Algebra.Notation.FiniteSupport Mathlib.Algebra.Order.Field.Pi Mathlib.Algebra.Order.Group.Multiset Mathlib.Algebra.PresentedMonoid.Basic Mathlib.Basic.Denumerable Mathlib.Basic.Finite.Set Mathlib.Basic.Finite.Sum Mathlib.CategoryTheory.Category.Cat.Adjunction Mathlib.CategoryTheory.ComposableArrows.Basic Mathlib.CategoryTheory.ComposableArrows.Four Mathlib.CategoryTheory.ComposableArrows.One Mathlib.CategoryTheory.ComposableArrows.Three Mathlib.CategoryTheory.ComposableArrows.Two Mathlib.CategoryTheory.ConnectedComponents Mathlib.CategoryTheory.Countable Mathlib.CategoryTheory.FinCategory.AsType Mathlib.CategoryTheory.FinCategory.Basic Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory Mathlib.CategoryTheory.Groupoid.Grpd.Basic Mathlib.CategoryTheory.IsConnected Mathlib.CategoryTheory.Limits.Bicones Mathlib.CategoryTheory.Limits.Connected Mathlib.CategoryTheory.Limits.Shapes.Connected Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer Mathlib.CategoryTheory.Limits.Shapes.SingleObj Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows Mathlib.CategoryTheory.SingleObj Mathlib.Combinatorics.Quiver.Path.Vertices Mathlib.Combinatorics.Quiver.Schreier Mathlib.Combinatorics.SetFamily.Compression.Down Mathlib.Combinatorics.SetFamily.Intersecting Mathlib.Combinatorics.Tiling.Tile Mathlib.Computability.TuringMachine.Tape Mathlib.Control.EquivFunctor.Instances Mathlib.Control.Fold Mathlib.Control.Functor.Multivariate Mathlib.Control.Traversable.Instances Mathlib.Data.DFinsupp.Defs Mathlib.Data.DFinsupp.Ext Mathlib.Data.DFinsupp.NeLocus Mathlib.Data.DFinsupp.Notation Mathlib.Data.Fin.Fin2 Mathlib.Data.Fin.Pigeonhole Mathlib.Data.Finite.Set Mathlib.Data.Finite.Sum Mathlib.Data.Finset.Attach Mathlib.Data.Finset.Basic Mathlib.Data.Finset.BooleanAlgebra Mathlib.Data.Finset.Card Mathlib.Data.Finset.CastCard Mathlib.Data.Finset.Dedup Mathlib.Data.Finset.Defs Mathlib.Data.Finset.DenselyOrdered Mathlib.Data.Finset.Disjoint Mathlib.Data.Finset.Empty Mathlib.Data.Finset.Erase Mathlib.Data.Finset.Filter Mathlib.Data.Finset.Fin Mathlib.Data.Finset.Fold Mathlib.Data.Finset.Image Mathlib.Data.Finset.Insert Mathlib.Data.Finset.Lattice.Basic Mathlib.Data.Finset.Lattice.Fold Mathlib.Data.Finset.Lattice.Lemmas Mathlib.Data.Finset.Max Mathlib.Data.Finset.Order Mathlib.Data.Finset.Pairwise Mathlib.Data.Finset.Piecewise Mathlib.Data.Finset.Range Mathlib.Data.Finset.SDiff Mathlib.Data.Finset.Sort Mathlib.Data.Finset.Sum Mathlib.Data.Finset.SymmDiff Mathlib.Data.Finsupp.Defs Mathlib.Data.Finsupp.Ext Mathlib.Data.Finsupp.Fin Mathlib.Data.Finsupp.Indicator Mathlib.Data.Finsupp.NeLocus Mathlib.Data.Finsupp.Notation Mathlib.Data.Finsupp.Quotient Mathlib.Data.Finsupp.Single Mathlib.Data.Fintype.Basic Mathlib.Data.Fintype.Card Mathlib.Data.Fintype.Defs Mathlib.Data.Fintype.EquivFin Mathlib.Data.Fintype.Inv Mathlib.Data.Fintype.Lattice Mathlib.Data.Fintype.OfMap Mathlib.Data.Fintype.Parity Mathlib.Data.Fintype.Perm Mathlib.Data.Fintype.Sets Mathlib.Data.Fintype.Shrink Mathlib.Data.Fintype.Sort Mathlib.Data.Fintype.Sum Mathlib.Data.List.AList Mathlib.Data.List.Basic Mathlib.Data.List.Chain Mathlib.Data.List.Dedup Mathlib.Data.List.Destutter Mathlib.Data.List.Duplicate Mathlib.Data.List.Enum Mathlib.Data.List.FinRange Mathlib.Data.List.Infix Mathlib.Data.List.Intervals Mathlib.Data.List.Lattice Mathlib.Data.List.Lemmas Mathlib.Data.List.Lex Mathlib.Data.List.MinMax Mathlib.Data.List.NatAntidiagonal Mathlib.Data.List.NodupEquivFin Mathlib.Data.List.Nodup Mathlib.Data.List.OffDiag Mathlib.Data.List.Perm.Lattice Mathlib.Data.List.Perm.Subperm Mathlib.Data.List.Permutation Mathlib.Data.List.Range Mathlib.Data.List.ReduceOption Mathlib.Data.List.Rotate Mathlib.Data.List.Sigma Mathlib.Data.List.Sort Mathlib.Data.List.SplitBy Mathlib.Data.List.Sublists Mathlib.Data.List.ToFinsupp Mathlib.Data.List.Zip Mathlib.Data.Multiset.AddSub Mathlib.Data.Multiset.Basic Mathlib.Data.Multiset.Count Mathlib.Data.Multiset.Dedup Mathlib.Data.Multiset.Defs Mathlib.Data.Multiset.DershowitzManna Mathlib.Data.Multiset.Filter Mathlib.Data.Multiset.Find Mathlib.Data.Multiset.FinsetOps Mathlib.Data.Multiset.Fold Mathlib.Data.Multiset.Lattice Mathlib.Data.Multiset.MapFold Mathlib.Data.Multiset.NatAntidiagonal Mathlib.Data.Multiset.OrderedMonoid Mathlib.Data.Multiset.Pairwise Mathlib.Data.Multiset.Range Mathlib.Data.Multiset.Replicate Mathlib.Data.Multiset.Sort Mathlib.Data.Multiset.Sum Mathlib.Data.Multiset.UnionInter Mathlib.Data.Multiset.ZeroCons Mathlib.Data.Nat.Count Mathlib.Data.Prod.TProd Mathlib.Data.Set.Constructions Mathlib.Data.Set.Countable Mathlib.Data.Set.Finite.Basic Mathlib.Data.Set.Finite.Range Mathlib.Data.Set.Pairwise.List Mathlib.Data.String.Basic Mathlib.Data.TypeVec Mathlib.Data.Vector3 Mathlib.GroupTheory.Coprod.Basic Mathlib.GroupTheory.DedekindFinite Mathlib.GroupTheory.FreeGroup.Basic Mathlib.GroupTheory.FreeGroup.IsFreeGroup Mathlib.GroupTheory.FreeGroup.Orbit Mathlib.GroupTheory.FreeGroup.Reduce Mathlib.GroupTheory.GroupAction.ConjAct Mathlib.GroupTheory.PresentedGroup Mathlib.Logic.Equiv.Array Mathlib.Logic.Equiv.Finset Mathlib.Logic.Equiv.Fintype Mathlib.Logic.Equiv.List Mathlib.Logic.Equiv.Multiset Mathlib.MeasureTheory.MeasurableSpace.Defs Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable Mathlib.MeasureTheory.MeasurableSpace.Invariants Mathlib.Order.CountableDenseLinearOrder Mathlib.Order.Filter.CountableInter Mathlib.Order.Filter.CountableSeparatingOn Mathlib.Order.Filter.Extr Mathlib.Order.Filter.ListTraverse Mathlib.Order.Fin.Finset Mathlib.Order.Fin.SuccAboveOrderIso Mathlib.Order.Ideal Mathlib.Order.Interval.Finset.Gaps Mathlib.Order.Interval.Set.Infinite Mathlib.Order.Interval.Set.Union Mathlib.Order.Irreducible Mathlib.Order.NonemptyFiniteChains Mathlib.Order.PFilter Mathlib.Order.Preorder.Finite Mathlib.Order.Preorder.Finsupp Mathlib.Order.PrimeIdeal Mathlib.Order.PrimeSeparator Mathlib.Tactic.DeriveFintype Mathlib.Tactic.FinCases Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.Algebra.Group.Defs Mathlib.Topology.Algebra.Monoid.Defs Mathlib.Topology.Basic Mathlib.Topology.Closure Mathlib.Topology.ClusterPt Mathlib.Topology.Constructions.SumProd Mathlib.Topology.Continuous Mathlib.Topology.Defs.Induced Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.Topology.Homeomorph.Defs Mathlib.Topology.Homeomorph.TransferInstance Mathlib.Topology.Instances.Shrink Mathlib.Topology.Maps.Basic Mathlib.Topology.Maps.OpenQuotient Mathlib.Topology.MetricSpace.BundledFun Mathlib.Topology.Neighborhoods Mathlib.Topology.NhdsSet Mathlib.Topology.Order.Hom.Basic Mathlib.Topology.Order.Hom.Esakia Mathlib.Topology.Order Mathlib.Topology.Partial Mathlib.Topology.Separation.SeparatedNhds Mathlib.Topology.UniformSpace.Defs Mathlib.Topology.UniformSpace.OfFun Mathlib.Topology.WithTopology
 1

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 45755497a2
Reference commit 64401b008c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@kim-em @claude
chore: keep the core inclusion family import
4575549 
`Mathlib.Tactic.Inclusion.Extension.Core.Init` exists only to run
`registerInclusionFamily `core`, and `Core.lean` names that family through the
literal `` `core ``, so shake sees no traced dependency and drops the import,
leaving `Unknown inclusion family `core``. Annotate the import as
`shake: keep`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TAGRpFSArN4EqRLSLJbBrq
@kim-em kim-em mentioned this pull request Sep 13, 2026
Open
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

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@kim-em