Documentation

Mathlib

source

Imports

Init
Mathlib.Algebra.Abs
Mathlib.Algebra.AddTorsor
Mathlib.Algebra.Associated
Mathlib.Algebra.Bounds
Mathlib.Algebra.CovariantAndContravariant
Mathlib.Algebra.CubicDiscriminant
Mathlib.Algebra.DualNumber
Mathlib.Algebra.Free
Mathlib.Algebra.FreeAlgebra
Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
Mathlib.Algebra.GeomSum
Mathlib.Algebra.GradedMonoid
Mathlib.Algebra.GradedMulAction
Mathlib.Algebra.HierarchyDesign
Mathlib.Algebra.IndicatorFunction
Mathlib.Algebra.Invertible
Mathlib.Algebra.IsPrimePow
Mathlib.Algebra.NeZero
Mathlib.Algebra.Opposites
Mathlib.Algebra.PEmptyInstances
Mathlib.Algebra.PUnitInstances
Mathlib.Algebra.Parity
Mathlib.Algebra.Periodic
Mathlib.Algebra.QuadraticDiscriminant
Mathlib.Algebra.Quandle
Mathlib.Algebra.Quotient
Mathlib.Algebra.SMulWithZero
Mathlib.Algebra.Squarefree
Mathlib.Algebra.Support
Mathlib.Algebra.TrivSqZeroExt
Mathlib.Analysis.Subadditive
Mathlib.CategoryTheory.Arrow
Mathlib.CategoryTheory.Balanced
Mathlib.CategoryTheory.CommSq
Mathlib.CategoryTheory.Comma
Mathlib.CategoryTheory.Conj
Mathlib.CategoryTheory.ConnectedComponents
Mathlib.CategoryTheory.Core
Mathlib.CategoryTheory.DiscreteCategory
Mathlib.CategoryTheory.Elementwise
Mathlib.CategoryTheory.Endomorphism
Mathlib.CategoryTheory.EpiMono
Mathlib.CategoryTheory.EqToHom
Mathlib.CategoryTheory.Equivalence
Mathlib.CategoryTheory.EssentialImage
Mathlib.CategoryTheory.EssentiallySmall
Mathlib.CategoryTheory.Filtered
Mathlib.CategoryTheory.FinCategory
Mathlib.CategoryTheory.FullSubcategory
Mathlib.CategoryTheory.GlueData
Mathlib.CategoryTheory.Groupoid
Mathlib.CategoryTheory.IsConnected
Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.IsomorphismClasses
Mathlib.CategoryTheory.MorphismProperty
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.NatTrans
Mathlib.CategoryTheory.Opposites
Mathlib.CategoryTheory.Over
Mathlib.CategoryTheory.PEmpty
Mathlib.CategoryTheory.PUnit
Mathlib.CategoryTheory.PathCategory
Mathlib.CategoryTheory.Quotient
Mathlib.CategoryTheory.SingleObj
Mathlib.CategoryTheory.Skeletal
Mathlib.CategoryTheory.StructuredArrow
Mathlib.CategoryTheory.Thin
Mathlib.CategoryTheory.Types
Mathlib.CategoryTheory.Whiskering
Mathlib.CategoryTheory.Yoneda
Mathlib.Combinatorics.Catalan
Mathlib.Combinatorics.Colex
Mathlib.Combinatorics.Composition
Mathlib.Combinatorics.DoubleCounting
Mathlib.Combinatorics.HalesJewett
Mathlib.Combinatorics.Hindman
Mathlib.Combinatorics.Partition
Mathlib.Combinatorics.Pigeonhole
Mathlib.Computability.DFA
Mathlib.Computability.EpsilonNFA
Mathlib.Computability.Language
Mathlib.Computability.NFA
Mathlib.Computability.Primrec
Mathlib.Computability.TuringMachine
Mathlib.Control.Applicative
Mathlib.Control.Basic
Mathlib.Control.Bifunctor
Mathlib.Control.EquivFunctor
Mathlib.Control.Fix
Mathlib.Control.Functor
Mathlib.Control.LawfulFix
Mathlib.Control.Random
Mathlib.Control.SimpSet
Mathlib.Control.ULift
Mathlib.Control.Writer
Mathlib.Data.BinaryHeap
Mathlib.Data.Bracket
Mathlib.Data.Bundle
Mathlib.Data.ByteArray
Mathlib.Data.Char
Mathlib.Data.Erased
Mathlib.Data.FinEnum
Mathlib.Data.Finmap
Mathlib.Data.HashMap
Mathlib.Data.Holor
Mathlib.Data.KVMap
Mathlib.Data.LazyList
Mathlib.Data.ListM
Mathlib.Data.Opposite
Mathlib.Data.PEquiv
Mathlib.Data.PFun
Mathlib.Data.Part
Mathlib.Data.Quot
Mathlib.Data.Rel
Mathlib.Data.Semiquot
Mathlib.Data.Sign
Mathlib.Data.Subtype
Mathlib.Data.Tree
Mathlib.Data.TwoPointing
Mathlib.Data.TypeVec
Mathlib.Data.UInt
Mathlib.Data.ULift
Mathlib.Data.UnionFind
Mathlib.Data.Vector
Mathlib.Deprecated.Group
Mathlib.Deprecated.Ring
Mathlib.Deprecated.Subfield
Mathlib.Deprecated.Subgroup
Mathlib.Deprecated.Submonoid
Mathlib.Deprecated.Subring
Mathlib.Dynamics.Flow
Mathlib.Dynamics.Minimal
Mathlib.Dynamics.OmegaLimit
Mathlib.Dynamics.PeriodicPts
Mathlib.FieldTheory.PerfectClosure
Mathlib.FieldTheory.Subfield
Mathlib.GroupTheory.Abelianization
Mathlib.GroupTheory.Archimedean
Mathlib.GroupTheory.Commensurable
Mathlib.GroupTheory.Commutator
Mathlib.GroupTheory.CommutingProbability
Mathlib.GroupTheory.Congruence
Mathlib.GroupTheory.Coset
Mathlib.GroupTheory.Divisible
Mathlib.GroupTheory.DoubleCoset
Mathlib.GroupTheory.EckmannHilton
Mathlib.GroupTheory.Finiteness
Mathlib.GroupTheory.FreeAbelianGroup
Mathlib.GroupTheory.FreeGroup
Mathlib.GroupTheory.FreeProduct
Mathlib.GroupTheory.Index
Mathlib.GroupTheory.IsFreeGroup
Mathlib.GroupTheory.MonoidLocalization
Mathlib.GroupTheory.NoncommPiCoprod
Mathlib.GroupTheory.OrderOfElement
Mathlib.GroupTheory.PresentedGroup
Mathlib.GroupTheory.QuotientGroup
Mathlib.GroupTheory.SemidirectProduct
Mathlib.GroupTheory.Solvable
Mathlib.InformationTheory.Hamming
Mathlib.Init.Align
Mathlib.Init.CcLemmas
Mathlib.Init.Classical
Mathlib.Init.Core
Mathlib.Init.Function
Mathlib.Init.Logic
Mathlib.Init.Propext
Mathlib.Init.Quot
Mathlib.Init.Set
Mathlib.Init.ZeroOne
Mathlib.Lean.EnvExtension
Mathlib.Lean.Exception
Mathlib.Lean.Expr
Mathlib.Lean.Linter
Mathlib.Lean.LocalContext
Mathlib.Lean.Message
Mathlib.Lean.Meta
Mathlib.LinearAlgebra.Basic
Mathlib.LinearAlgebra.Basis
Mathlib.LinearAlgebra.BilinearMap
Mathlib.LinearAlgebra.Dfinsupp
Mathlib.LinearAlgebra.Finsupp
Mathlib.LinearAlgebra.GeneralLinearGroup
Mathlib.LinearAlgebra.InvariantBasisNumber
Mathlib.LinearAlgebra.LinearIndependent
Mathlib.LinearAlgebra.LinearPMap
Mathlib.LinearAlgebra.Pi
Mathlib.LinearAlgebra.Prod
Mathlib.LinearAlgebra.Projection
Mathlib.LinearAlgebra.Quotient
Mathlib.LinearAlgebra.Ray
Mathlib.LinearAlgebra.SModEq
Mathlib.LinearAlgebra.SesquilinearForm
Mathlib.LinearAlgebra.Span
Mathlib.LinearAlgebra.TensorProduct
Mathlib.Logic.Basic
Mathlib.Logic.Denumerable
Mathlib.Logic.IsEmpty
Mathlib.Logic.Lemmas
Mathlib.Logic.Nonempty
Mathlib.Logic.Nontrivial
Mathlib.Logic.Pairwise
Mathlib.Logic.Relation
Mathlib.Logic.Relator
Mathlib.Logic.Unique
Mathlib.Mathport.Attributes
Mathlib.Mathport.Notation
Mathlib.Mathport.Rename
Mathlib.Mathport.Syntax
Mathlib.MeasureTheory.CardMeasurableSpace
Mathlib.MeasureTheory.MeasurableSpace
Mathlib.MeasureTheory.MeasurableSpaceDef
Mathlib.MeasureTheory.PiSystem
Mathlib.ModelTheory.Basic
Mathlib.NumberTheory.ADEInequality
Mathlib.NumberTheory.Basic
Mathlib.NumberTheory.Divisors
Mathlib.NumberTheory.Fermat4
Mathlib.NumberTheory.FrobeniusNumber
Mathlib.NumberTheory.LucasPrimality
Mathlib.NumberTheory.Primorial
Mathlib.NumberTheory.PythagoreanTriples
Mathlib.Order.Antichain
Mathlib.Order.Antisymmetrization
Mathlib.Order.Atoms
Mathlib.Order.Basic
Mathlib.Order.BooleanAlgebra
Mathlib.Order.Bounded
Mathlib.Order.BoundedOrder
Mathlib.Order.Chain
Mathlib.Order.Circular
Mathlib.Order.Closure
Mathlib.Order.CompactlyGenerated
Mathlib.Order.Compare
Mathlib.Order.CompleteBooleanAlgebra
Mathlib.Order.CompleteLattice
Mathlib.Order.CompleteLatticeIntervals
Mathlib.Order.Concept
Mathlib.Order.Copy
Mathlib.Order.CountableDenseLinearOrder
Mathlib.Order.Cover
Mathlib.Order.Directed
Mathlib.Order.Disjoint
Mathlib.Order.Disjointed
Mathlib.Order.FixedPoints
Mathlib.Order.GaloisConnection
Mathlib.Order.GameAdd
Mathlib.Order.Grade
Mathlib.Order.Ideal
Mathlib.Order.InitialSeg
Mathlib.Order.Iterate
Mathlib.Order.JordanHolder
Mathlib.Order.Lattice
Mathlib.Order.LatticeIntervals
Mathlib.Order.LiminfLimsup
Mathlib.Order.LocallyFinite
Mathlib.Order.Max
Mathlib.Order.MinMax
Mathlib.Order.Minimal
Mathlib.Order.ModularLattice
Mathlib.Order.OmegaCompletePartialOrder
Mathlib.Order.OrdContinuous
Mathlib.Order.OrderIsoNat
Mathlib.Order.PFilter
Mathlib.Order.PartialSups
Mathlib.Order.PrimeIdeal
Mathlib.Order.PropInstances
Mathlib.Order.RelClasses
Mathlib.Order.SemiconjSup
Mathlib.Order.SupIndep
Mathlib.Order.SymmDiff
Mathlib.Order.Synonym
Mathlib.Order.WellFounded
Mathlib.Order.WellFoundedSet
Mathlib.Order.WithBot
Mathlib.Order.Zorn
Mathlib.Order.ZornAtoms
Mathlib.RepresentationTheory.Maschke
Mathlib.RingTheory.AlgebraTower
Mathlib.RingTheory.Congruence
Mathlib.RingTheory.EuclideanDomain
Mathlib.RingTheory.Finiteness
Mathlib.RingTheory.Fintype
Mathlib.RingTheory.Flat
Mathlib.RingTheory.FreeRing
Mathlib.RingTheory.Multiplicity
Mathlib.RingTheory.Nilpotent
Mathlib.RingTheory.Noetherian
Mathlib.RingTheory.NonZeroDivisors
Mathlib.RingTheory.Prime
Mathlib.RingTheory.PrincipalIdealDomain
Mathlib.RingTheory.RingInvo
Mathlib.RingTheory.UniqueFactorizationDomain
Mathlib.SetTheory.Lists
Mathlib.Tactic.Abel
Mathlib.Tactic.Alias
Mathlib.Tactic.ApplyFun
Mathlib.Tactic.ApplyWith
Mathlib.Tactic.Basic
Mathlib.Tactic.ByContra
Mathlib.Tactic.Cache
Mathlib.Tactic.Cases
Mathlib.Tactic.CasesM
Mathlib.Tactic.Choose
Mathlib.Tactic.Classical
Mathlib.Tactic.Clear!
Mathlib.Tactic.ClearExcept
Mathlib.Tactic.Clear_
Mathlib.Tactic.Coe
Mathlib.Tactic.Congr!
Mathlib.Tactic.Constructor
Mathlib.Tactic.Continuity
Mathlib.Tactic.Contrapose
Mathlib.Tactic.Conv
Mathlib.Tactic.Convert
Mathlib.Tactic.Core
Mathlib.Tactic.Elementwise
Mathlib.Tactic.Existsi
Mathlib.Tactic.FailIfNoProgress
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FinCases
Mathlib.Tactic.Find
Mathlib.Tactic.GeneralizeProofs
Mathlib.Tactic.Group
Mathlib.Tactic.GuardGoalNums
Mathlib.Tactic.GuardHypNums
Mathlib.Tactic.Have
Mathlib.Tactic.HelpCmd
Mathlib.Tactic.HigherOrder
Mathlib.Tactic.InferParam
Mathlib.Tactic.Inhabit
Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IrreducibleDef
Mathlib.Tactic.LabelAttr
Mathlib.Tactic.LeftRight
Mathlib.Tactic.LibrarySearch
Mathlib.Tactic.Lift
Mathlib.Tactic.Linarith
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.MkIffOfInductiveProp
Mathlib.Tactic.ModCases
Mathlib.Tactic.Monotonicity
Mathlib.Tactic.Nontriviality
Mathlib.Tactic.NormCast
Mathlib.Tactic.NormNum
Mathlib.Tactic.NthRewrite
Mathlib.Tactic.PermuteGoals
Mathlib.Tactic.Polyrith
Mathlib.Tactic.Positivity
Mathlib.Tactic.PrintPrefix
Mathlib.Tactic.PushNeg
Mathlib.Tactic.Qify
Mathlib.Tactic.RSuffices
Mathlib.Tactic.Reassoc
Mathlib.Tactic.Recover
Mathlib.Tactic.Rename
Mathlib.Tactic.RenameBVar
Mathlib.Tactic.Replace
Mathlib.Tactic.RestateAxiom
Mathlib.Tactic.Ring
Mathlib.Tactic.RunCmd
Mathlib.Tactic.ScopedNS
Mathlib.Tactic.Set
Mathlib.Tactic.SimpIntro
Mathlib.Tactic.SimpRw
Mathlib.Tactic.Slice
Mathlib.Tactic.SolveByElim
Mathlib.Tactic.SplitIfs
Mathlib.Tactic.Spread
Mathlib.Tactic.Substs
Mathlib.Tactic.SuccessIfFailWithMsg
Mathlib.Tactic.SudoSetOption
Mathlib.Tactic.SwapVar
Mathlib.Tactic.TFAE
Mathlib.Tactic.Tauto
Mathlib.Tactic.ToAdditive
Mathlib.Tactic.Trace
Mathlib.Tactic.TypeCheck
Mathlib.Tactic.UnsetOption
Mathlib.Tactic.Use
Mathlib.Tactic.WLOG
Mathlib.Tactic.Zify
Mathlib.Topology.Alexandroff
Mathlib.Topology.Bases
Mathlib.Topology.Basic
Mathlib.Topology.CompactOpen
Mathlib.Topology.Connected
Mathlib.Topology.Constructions
Mathlib.Topology.ContinuousOn
Mathlib.Topology.Covering
Mathlib.Topology.DenseEmbedding
Mathlib.Topology.DiscreteQuotient
Mathlib.Topology.ExtendFrom
Mathlib.Topology.Filter
Mathlib.Topology.GDelta
Mathlib.Topology.Homeomorph
Mathlib.Topology.Inseparable
Mathlib.Topology.IsLocallyHomeomorph
Mathlib.Topology.List
Mathlib.Topology.LocalExtr
Mathlib.Topology.LocalHomeomorph
Mathlib.Topology.LocallyFinite
Mathlib.Topology.Maps
Mathlib.Topology.NhdsSet
Mathlib.Topology.NoetherianSpace
Mathlib.Topology.OmegaCompletePartialOrder
Mathlib.Topology.Order
Mathlib.Topology.Paracompact
Mathlib.Topology.Partial
Mathlib.Topology.PathConnected
Mathlib.Topology.Perfect
Mathlib.Topology.QuasiSeparated
Mathlib.Topology.Semicontinuous
Mathlib.Topology.Separation
Mathlib.Topology.Sequences
Mathlib.Topology.ShrinkingLemma
Mathlib.Topology.Sober
Mathlib.Topology.StoneCech
Mathlib.Topology.SubsetProperties
Mathlib.Topology.Support
Mathlib.Topology.Tactic
Mathlib.Topology.UnitInterval
Mathlib.Util.AddRelatedDecl
Mathlib.Util.AssertNoSorry
Mathlib.Util.AtomM
Mathlib.Util.Export
Mathlib.Util.IncludeStr
Mathlib.Util.MemoFix
Mathlib.Util.Syntax
Mathlib.Util.SynthesizeUsing
Mathlib.Util.Tactic
Mathlib.Util.Time
Mathlib.Util.WhatsNew
Mathlib.Util.WithWeakNamespace
Mathlib.Algebra.Algebra.Basic
Mathlib.Algebra.Algebra.Bilinear
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Algebra.Hom
Mathlib.Algebra.Algebra.Operations
Mathlib.Algebra.Algebra.Pi
Mathlib.Algebra.Algebra.Prod
Mathlib.Algebra.Algebra.RestrictScalars
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.Algebra.Unitization
Mathlib.Algebra.BigOperators.Associated
Mathlib.Algebra.BigOperators.Basic
Mathlib.Algebra.BigOperators.Fin
Mathlib.Algebra.BigOperators.Finprod
Mathlib.Algebra.BigOperators.Finsupp
Mathlib.Algebra.BigOperators.Intervals
Mathlib.Algebra.BigOperators.NatAntidiagonal
Mathlib.Algebra.BigOperators.Option
Mathlib.Algebra.BigOperators.Order
Mathlib.Algebra.BigOperators.Pi
Mathlib.Algebra.BigOperators.Ring
Mathlib.Algebra.BigOperators.RingEquiv
Mathlib.Algebra.CharP.Algebra
Mathlib.Algebra.CharP.Basic
Mathlib.Algebra.CharP.ExpChar
Mathlib.Algebra.CharP.Invertible
Mathlib.Algebra.CharP.Pi
Mathlib.Algebra.CharP.Quotient
Mathlib.Algebra.CharP.Subring
Mathlib.Algebra.CharP.Two
Mathlib.Algebra.CharZero.Defs
Mathlib.Algebra.CharZero.Infinite
Mathlib.Algebra.CharZero.Lemmas
Mathlib.Algebra.CharZero.Quotient
Mathlib.Algebra.DirectSum.Basic
Mathlib.Algebra.DirectSum.Finsupp
Mathlib.Algebra.DirectSum.Module
Mathlib.Algebra.Divisibility.Basic
Mathlib.Algebra.Divisibility.Units
Mathlib.Algebra.EuclideanDomain.Basic
Mathlib.Algebra.EuclideanDomain.Defs
Mathlib.Algebra.EuclideanDomain.Instances
Mathlib.Algebra.Field.Basic
Mathlib.Algebra.Field.Defs
Mathlib.Algebra.Field.Opposite
Mathlib.Algebra.Field.Power
Mathlib.Algebra.Field.ULift
Mathlib.Algebra.FreeMonoid.Basic
Mathlib.Algebra.FreeMonoid.Count
Mathlib.Algebra.GCDMonoid.Basic
Mathlib.Algebra.GCDMonoid.Div
Mathlib.Algebra.GCDMonoid.Finset
Mathlib.Algebra.GCDMonoid.Multiset
Mathlib.Algebra.Group.Basic
Mathlib.Algebra.Group.Commutator
Mathlib.Algebra.Group.Commute
Mathlib.Algebra.Group.Conj
Mathlib.Algebra.Group.ConjFinite
Mathlib.Algebra.Group.Defs
Mathlib.Algebra.Group.Ext
Mathlib.Algebra.Group.InjSurj
Mathlib.Algebra.Group.Opposite
Mathlib.Algebra.Group.OrderSynonym
Mathlib.Algebra.Group.Pi
Mathlib.Algebra.Group.Prod
Mathlib.Algebra.Group.Semiconj
Mathlib.Algebra.Group.TypeTags
Mathlib.Algebra.Group.ULift
Mathlib.Algebra.Group.UniqueProds
Mathlib.Algebra.Group.Units
Mathlib.Algebra.GroupPower.Basic
Mathlib.Algebra.GroupPower.Identities
Mathlib.Algebra.GroupPower.Lemmas
Mathlib.Algebra.GroupPower.Order
Mathlib.Algebra.GroupPower.Ring
Mathlib.Algebra.GroupRingAction.Basic
Mathlib.Algebra.GroupRingAction.Invariant
Mathlib.Algebra.GroupRingAction.Subobjects
Mathlib.Algebra.GroupWithZero.Basic
Mathlib.Algebra.GroupWithZero.Commute
Mathlib.Algebra.GroupWithZero.Defs
Mathlib.Algebra.GroupWithZero.Divisibility
Mathlib.Algebra.GroupWithZero.InjSurj
Mathlib.Algebra.GroupWithZero.Power
Mathlib.Algebra.GroupWithZero.Semiconj
Mathlib.Algebra.Hom.Aut
Mathlib.Algebra.Hom.Centroid
Mathlib.Algebra.Hom.Commute
Mathlib.Algebra.Hom.Embedding
Mathlib.Algebra.Hom.Freiman
Mathlib.Algebra.Hom.Group
Mathlib.Algebra.Hom.GroupAction
Mathlib.Algebra.Hom.GroupInstances
Mathlib.Algebra.Hom.Iterate
Mathlib.Algebra.Hom.NonUnitalAlg
Mathlib.Algebra.Hom.Ring
Mathlib.Algebra.Hom.Units
Mathlib.Algebra.Homology.ComplexShape
Mathlib.Algebra.Lie.Basic
Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
Mathlib.Algebra.Lie.Subalgebra
Mathlib.Algebra.Module.Algebra
Mathlib.Algebra.Module.Basic
Mathlib.Algebra.Module.BigOperators
Mathlib.Algebra.Module.Equiv
Mathlib.Algebra.Module.Hom
Mathlib.Algebra.Module.LinearMap
Mathlib.Algebra.Module.Opposites
Mathlib.Algebra.Module.Pi
Mathlib.Algebra.Module.PointwisePi
Mathlib.Algebra.Module.Prod
Mathlib.Algebra.Module.ULift
Mathlib.Algebra.MonoidAlgebra.Basic
Mathlib.Algebra.MonoidAlgebra.Degree
Mathlib.Algebra.MonoidAlgebra.Division
Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Mathlib.Algebra.MonoidAlgebra.Support
Mathlib.Algebra.Order.AbsoluteValue
Mathlib.Algebra.Order.Algebra
Mathlib.Algebra.Order.Archimedean
Mathlib.Algebra.Order.EuclideanAbsoluteValue
Mathlib.Algebra.Order.Floor
Mathlib.Algebra.Order.Invertible
Mathlib.Algebra.Order.Kleene
Mathlib.Algebra.Order.LatticeGroup
Mathlib.Algebra.Order.Module
Mathlib.Algebra.Order.Pi
Mathlib.Algebra.Order.Pointwise
Mathlib.Algebra.Order.SMul
Mathlib.Algebra.Order.UpperLower
Mathlib.Algebra.Order.WithZero
Mathlib.Algebra.Order.ZeroLEOne
Mathlib.Algebra.Polynomial.BigOperators
Mathlib.Algebra.Polynomial.GroupRingAction
Mathlib.Algebra.Regular.Basic
Mathlib.Algebra.Regular.Pow
Mathlib.Algebra.Regular.SMul
Mathlib.Algebra.Ring.AddAut
Mathlib.Algebra.Ring.Aut
Mathlib.Algebra.Ring.Basic
Mathlib.Algebra.Ring.Commute
Mathlib.Algebra.Ring.CompTypeclasses
Mathlib.Algebra.Ring.Defs
Mathlib.Algebra.Ring.Divisibility
Mathlib.Algebra.Ring.Equiv
Mathlib.Algebra.Ring.Fin
Mathlib.Algebra.Ring.Idempotents
Mathlib.Algebra.Ring.InjSurj
Mathlib.Algebra.Ring.Opposite
Mathlib.Algebra.Ring.OrderSynonym
Mathlib.Algebra.Ring.Pi
Mathlib.Algebra.Ring.Prod
Mathlib.Algebra.Ring.Regular
Mathlib.Algebra.Ring.Semiconj
Mathlib.Algebra.Ring.ULift
Mathlib.Algebra.Ring.Units
Mathlib.Algebra.Star.Basic
Mathlib.Algebra.Star.BigOperators
Mathlib.Algebra.Star.CHSH
Mathlib.Algebra.Star.Free
Mathlib.Algebra.Star.Module
Mathlib.Algebra.Star.Pi
Mathlib.Algebra.Star.Pointwise
Mathlib.Algebra.Star.Prod
Mathlib.Algebra.Star.SelfAdjoint
Mathlib.Algebra.Star.StarAlgHom
Mathlib.Algebra.Star.Subalgebra
Mathlib.Algebra.Star.Unitary
Mathlib.Algebra.Tropical.Basic
Mathlib.Algebra.Tropical.BigOperators
Mathlib.Algebra.Tropical.Lattice
Mathlib.Analysis.Convex.Basic
Mathlib.Analysis.Convex.Extreme
Mathlib.Analysis.Convex.Hull
Mathlib.Analysis.Convex.Segment
Mathlib.Analysis.Convex.Star
Mathlib.Analysis.Convex.Strict
Mathlib.Analysis.NormedSpace.IndicatorFunction
Mathlib.Analysis.NormedSpace.Int
Mathlib.Analysis.NormedSpace.MStructure
Mathlib.CategoryTheory.Abelian.Images
Mathlib.CategoryTheory.Abelian.NonPreadditive
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Adjunction.Comma
Mathlib.CategoryTheory.Adjunction.Evaluation
Mathlib.CategoryTheory.Adjunction.FullyFaithful
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Adjunction.Mates
Mathlib.CategoryTheory.Adjunction.Opposites
Mathlib.CategoryTheory.Adjunction.Reflective
Mathlib.CategoryTheory.Adjunction.Whiskering
Mathlib.CategoryTheory.Bicategory.Basic
Mathlib.CategoryTheory.Bicategory.End
Mathlib.CategoryTheory.Bicategory.Functor
Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Mathlib.CategoryTheory.Bicategory.Strict
Mathlib.CategoryTheory.Category.Basic
Mathlib.CategoryTheory.Category.Bipointed
Mathlib.CategoryTheory.Category.Cat
Mathlib.CategoryTheory.Category.GaloisConnection
Mathlib.CategoryTheory.Category.Init
Mathlib.CategoryTheory.Category.KleisliCat
Mathlib.CategoryTheory.Category.Pairwise
Mathlib.CategoryTheory.Category.Pointed
Mathlib.CategoryTheory.Category.Preorder
Mathlib.CategoryTheory.Category.QuivCat
Mathlib.CategoryTheory.Category.RelCat
Mathlib.CategoryTheory.Category.TwoP
Mathlib.CategoryTheory.Category.ULift
Mathlib.CategoryTheory.Closed.Monoidal
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.ConcreteCategory.Bundled
Mathlib.CategoryTheory.ConcreteCategory.BundledHom
Mathlib.CategoryTheory.ConcreteCategory.Elementwise
Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
Mathlib.CategoryTheory.Functor.Basic
Mathlib.CategoryTheory.Functor.Category
Mathlib.CategoryTheory.Functor.Const
Mathlib.CategoryTheory.Functor.Currying
Mathlib.CategoryTheory.Functor.Default
Mathlib.CategoryTheory.Functor.EpiMono
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Functor.Functorial
Mathlib.CategoryTheory.Functor.Hom
Mathlib.CategoryTheory.Functor.InvIsos
Mathlib.CategoryTheory.Functor.ReflectsIso
Mathlib.CategoryTheory.Groupoid.Basic
Mathlib.CategoryTheory.Groupoid.VertexGroup
Mathlib.CategoryTheory.LiftingProperties.Adjunction
Mathlib.CategoryTheory.LiftingProperties.Basic
Mathlib.CategoryTheory.Limits.Bicones
Mathlib.CategoryTheory.Limits.ColimitLimit
Mathlib.CategoryTheory.Limits.Comma
Mathlib.CategoryTheory.Limits.ConcreteCategory
Mathlib.CategoryTheory.Limits.ConeCategory
Mathlib.CategoryTheory.Limits.Cones
Mathlib.CategoryTheory.Limits.Connected
Mathlib.CategoryTheory.Limits.Creates
Mathlib.CategoryTheory.Limits.EssentiallySmall
Mathlib.CategoryTheory.Limits.ExactFunctor
Mathlib.CategoryTheory.Limits.Filtered
Mathlib.CategoryTheory.Limits.Final
Mathlib.CategoryTheory.Limits.FullSubcategory
Mathlib.CategoryTheory.Limits.FunctorCategory
Mathlib.CategoryTheory.Limits.HasLimits
Mathlib.CategoryTheory.Limits.IsLimit
Mathlib.CategoryTheory.Limits.KanExtension
Mathlib.CategoryTheory.Limits.Lattice
Mathlib.CategoryTheory.Limits.MonoCoprod
Mathlib.CategoryTheory.Limits.Opposites
Mathlib.CategoryTheory.Limits.Pi
Mathlib.CategoryTheory.Limits.SmallComplete
Mathlib.CategoryTheory.Limits.Types
Mathlib.CategoryTheory.Limits.Unit
Mathlib.CategoryTheory.Limits.Yoneda
Mathlib.CategoryTheory.Linear.Basic
Mathlib.CategoryTheory.Linear.FunctorCategory
Mathlib.CategoryTheory.Linear.LinearFunctor
Mathlib.CategoryTheory.Localization.Construction
Mathlib.CategoryTheory.Localization.Opposite
Mathlib.CategoryTheory.Localization.Predicate
Mathlib.CategoryTheory.Monad.Basic
Mathlib.CategoryTheory.Monoidal.Category
Mathlib.CategoryTheory.Monoidal.Discrete
Mathlib.CategoryTheory.Monoidal.End
Mathlib.CategoryTheory.Monoidal.Functor
Mathlib.CategoryTheory.Monoidal.Functorial
Mathlib.CategoryTheory.Monoidal.Linear
Mathlib.CategoryTheory.Monoidal.NaturalTransformation
Mathlib.CategoryTheory.Monoidal.Preadditive
Mathlib.CategoryTheory.Monoidal.Transport
Mathlib.CategoryTheory.Pi.Basic
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Preadditive.Basic
Mathlib.CategoryTheory.Preadditive.Biproducts
Mathlib.CategoryTheory.Preadditive.FunctorCategory
Mathlib.CategoryTheory.Preadditive.LeftExact
Mathlib.CategoryTheory.Preadditive.OfBiproducts
Mathlib.CategoryTheory.Preadditive.SingleObj
Mathlib.CategoryTheory.Products.Associator
Mathlib.CategoryTheory.Products.Basic
Mathlib.CategoryTheory.Products.Bifunctor
Mathlib.CategoryTheory.Sigma.Basic
Mathlib.CategoryTheory.Sites.Grothendieck
Mathlib.CategoryTheory.Sites.Pretopology
Mathlib.CategoryTheory.Sites.Sieves
Mathlib.CategoryTheory.Sites.Spaces
Mathlib.CategoryTheory.Sums.Associator
Mathlib.CategoryTheory.Sums.Basic
Mathlib.Combinatorics.Additive.Energy
Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Mathlib.Combinatorics.Additive.RuzsaCovering
Mathlib.Combinatorics.Derangements.Basic
Mathlib.Combinatorics.Derangements.Finite
Mathlib.Combinatorics.Hall.Finite
Mathlib.Combinatorics.Quiver.Arborescence
Mathlib.Combinatorics.Quiver.Basic
Mathlib.Combinatorics.Quiver.Cast
Mathlib.Combinatorics.Quiver.ConnectedComponent
Mathlib.Combinatorics.Quiver.Path
Mathlib.Combinatorics.Quiver.Push
Mathlib.Combinatorics.Quiver.SingleObj
Mathlib.Combinatorics.Quiver.Subquiver
Mathlib.Combinatorics.Quiver.Symmetric
Mathlib.Combinatorics.SetFamily.HarrisKleitman
Mathlib.Combinatorics.SetFamily.Intersecting
Mathlib.Combinatorics.SetFamily.Kleitman
Mathlib.Combinatorics.SetFamily.LYM
Mathlib.Combinatorics.SetFamily.Shadow
Mathlib.Combinatorics.SimpleGraph.Acyclic
Mathlib.Combinatorics.SimpleGraph.Basic
Mathlib.Combinatorics.SimpleGraph.Clique
Mathlib.Combinatorics.SimpleGraph.Coloring
Mathlib.Combinatorics.SimpleGraph.Connectivity
Mathlib.Combinatorics.SimpleGraph.DegreeSum
Mathlib.Combinatorics.SimpleGraph.Density
Mathlib.Combinatorics.SimpleGraph.Hasse
Mathlib.Combinatorics.SimpleGraph.Init
Mathlib.Combinatorics.SimpleGraph.Matching
Mathlib.Combinatorics.SimpleGraph.Metric
Mathlib.Combinatorics.SimpleGraph.Partition
Mathlib.Combinatorics.SimpleGraph.Prod
Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Mathlib.Combinatorics.SimpleGraph.Subgraph
Mathlib.Combinatorics.SimpleGraph.Trails
Mathlib.Combinatorics.Young.SemistandardTableau
Mathlib.Combinatorics.Young.YoungDiagram
Mathlib.Control.Bitraversable.Basic
Mathlib.Control.EquivFunctor.Instances
Mathlib.Control.Functor.Multivariate
Mathlib.Control.Monad.Basic
Mathlib.Control.Traversable.Basic
Mathlib.Control.Traversable.Equiv
Mathlib.Control.Traversable.Instances
Mathlib.Control.Traversable.Lemmas
Mathlib.Data.Analysis.Filter
Mathlib.Data.Analysis.Topology
Mathlib.Data.Array.Basic
Mathlib.Data.Array.Defs
Mathlib.Data.Bitvec.Core
Mathlib.Data.Bool.AllAny
Mathlib.Data.Bool.Basic
Mathlib.Data.Bool.Count
Mathlib.Data.Bool.Set
Mathlib.Data.Complex.Basic
Mathlib.Data.Complex.Exponential
Mathlib.Data.Countable.Basic
Mathlib.Data.Countable.Defs
Mathlib.Data.Countable.Small
Mathlib.Data.DList.Basic
Mathlib.Data.DList.Instances
Mathlib.Data.Dfinsupp.Basic
Mathlib.Data.Dfinsupp.Interval
Mathlib.Data.Dfinsupp.Lex
Mathlib.Data.Dfinsupp.Multiset
Mathlib.Data.Dfinsupp.NeLocus
Mathlib.Data.Dfinsupp.Order
Mathlib.Data.Dfinsupp.WellFounded
Mathlib.Data.ENat.Basic
Mathlib.Data.ENat.Lattice
Mathlib.Data.Equiv.Functor
Mathlib.Data.FP.Basic
Mathlib.Data.Fin.Basic
Mathlib.Data.Fin.Fin2
Mathlib.Data.Fin.Interval
Mathlib.Data.Fin.SuccPred
Mathlib.Data.Fin.VecNotation
Mathlib.Data.Finite.Basic
Mathlib.Data.Finite.Card
Mathlib.Data.Finite.Defs
Mathlib.Data.Finite.Set
Mathlib.Data.Finset.Basic
Mathlib.Data.Finset.Card
Mathlib.Data.Finset.Fin
Mathlib.Data.Finset.Finsupp
Mathlib.Data.Finset.Fold
Mathlib.Data.Finset.Functor
Mathlib.Data.Finset.Image
Mathlib.Data.Finset.Lattice
Mathlib.Data.Finset.LocallyFinite
Mathlib.Data.Finset.MulAntidiagonal
Mathlib.Data.Finset.NAry
Mathlib.Data.Finset.NatAntidiagonal
Mathlib.Data.Finset.NoncommProd
Mathlib.Data.Finset.Option
Mathlib.Data.Finset.Order
Mathlib.Data.Finset.PImage
Mathlib.Data.Finset.Pairwise
Mathlib.Data.Finset.Pi
Mathlib.Data.Finset.PiInduction
Mathlib.Data.Finset.Pointwise
Mathlib.Data.Finset.Powerset
Mathlib.Data.Finset.Preimage
Mathlib.Data.Finset.Prod
Mathlib.Data.Finset.Sigma
Mathlib.Data.Finset.Slice
Mathlib.Data.Finset.Sort
Mathlib.Data.Finset.Sum
Mathlib.Data.Finset.Sym
Mathlib.Data.Finsupp.AList
Mathlib.Data.Finsupp.Antidiagonal
Mathlib.Data.Finsupp.Basic
Mathlib.Data.Finsupp.BigOperators
Mathlib.Data.Finsupp.Defs
Mathlib.Data.Finsupp.Fin
Mathlib.Data.Finsupp.Fintype
Mathlib.Data.Finsupp.Indicator
Mathlib.Data.Finsupp.Interval
Mathlib.Data.Finsupp.Lex
Mathlib.Data.Finsupp.Multiset
Mathlib.Data.Finsupp.NeLocus
Mathlib.Data.Finsupp.Order
Mathlib.Data.Finsupp.Pointwise
Mathlib.Data.Finsupp.Pwo
Mathlib.Data.Finsupp.ToDfinsupp
Mathlib.Data.Finsupp.WellFounded
Mathlib.Data.Fintype.Basic
Mathlib.Data.Fintype.BigOperators
Mathlib.Data.Fintype.Card
Mathlib.Data.Fintype.CardEmbedding
Mathlib.Data.Fintype.Fin
Mathlib.Data.Fintype.Lattice
Mathlib.Data.Fintype.List
Mathlib.Data.Fintype.Option
Mathlib.Data.Fintype.Order
Mathlib.Data.Fintype.Parity
Mathlib.Data.Fintype.Perm
Mathlib.Data.Fintype.Pi
Mathlib.Data.Fintype.Powerset
Mathlib.Data.Fintype.Prod
Mathlib.Data.Fintype.Sigma
Mathlib.Data.Fintype.Small
Mathlib.Data.Fintype.Sort
Mathlib.Data.Fintype.Sum
Mathlib.Data.Fintype.Units
Mathlib.Data.Fintype.Vector
Mathlib.Data.FunLike.Basic
Mathlib.Data.FunLike.Embedding
Mathlib.Data.FunLike.Equiv
Mathlib.Data.FunLike.Fintype
Mathlib.Data.Int.AbsoluteValue
Mathlib.Data.Int.Associated
Mathlib.Data.Int.Basic
Mathlib.Data.Int.Bitwise
Mathlib.Data.Int.CharZero
Mathlib.Data.Int.ConditionallyCompleteOrder
Mathlib.Data.Int.Div
Mathlib.Data.Int.GCD
Mathlib.Data.Int.Interval
Mathlib.Data.Int.LeastGreatest
Mathlib.Data.Int.Lemmas
Mathlib.Data.Int.Log
Mathlib.Data.Int.ModEq
Mathlib.Data.Int.NatPrime
Mathlib.Data.Int.Parity
Mathlib.Data.Int.Range
Mathlib.Data.Int.Sqrt
Mathlib.Data.Int.SuccPred
Mathlib.Data.Int.Units
Mathlib.Data.LazyList.Basic
Mathlib.Data.List.AList
Mathlib.Data.List.Basic
Mathlib.Data.List.Card
Mathlib.Data.List.Chain
Mathlib.Data.List.Count
Mathlib.Data.List.Cycle
Mathlib.Data.List.Dedup
Mathlib.Data.List.Defs
Mathlib.Data.List.Destutter
Mathlib.Data.List.Duplicate
Mathlib.Data.List.FinRange
Mathlib.Data.List.Forall2
Mathlib.Data.List.Func
Mathlib.Data.List.Indexes
Mathlib.Data.List.Infix
Mathlib.Data.List.Join
Mathlib.Data.List.Lattice
Mathlib.Data.List.Lemmas
Mathlib.Data.List.Lex
Mathlib.Data.List.MinMax
Mathlib.Data.List.NatAntidiagonal
Mathlib.Data.List.Nodup
Mathlib.Data.List.NodupEquivFin
Mathlib.Data.List.OfFn
Mathlib.Data.List.Pairwise
Mathlib.Data.List.Palindrome
Mathlib.Data.List.Perm
Mathlib.Data.List.Permutation
Mathlib.Data.List.Prime
Mathlib.Data.List.ProdSigma
Mathlib.Data.List.Range
Mathlib.Data.List.Rdrop
Mathlib.Data.List.Rotate
Mathlib.Data.List.Sections
Mathlib.Data.List.Sigma
Mathlib.Data.List.Sort
Mathlib.Data.List.Sublists
Mathlib.Data.List.TFAE
Mathlib.Data.List.Zip
Mathlib.Data.Matrix.DMatrix
Mathlib.Data.Multiset.Antidiagonal
Mathlib.Data.Multiset.Basic
Mathlib.Data.Multiset.Bind
Mathlib.Data.Multiset.Dedup
Mathlib.Data.Multiset.FinsetOps
Mathlib.Data.Multiset.Fintype
Mathlib.Data.Multiset.Fold
Mathlib.Data.Multiset.Functor
Mathlib.Data.Multiset.Interval
Mathlib.Data.Multiset.Lattice
Mathlib.Data.Multiset.LocallyFinite
Mathlib.Data.Multiset.NatAntidiagonal
Mathlib.Data.Multiset.Nodup
Mathlib.Data.Multiset.Pi
Mathlib.Data.Multiset.Powerset
Mathlib.Data.Multiset.Range
Mathlib.Data.Multiset.Sections
Mathlib.Data.Multiset.Sort
Mathlib.Data.Multiset.Sum
Mathlib.Data.MvPolynomial.Basic
Mathlib.Data.MvPolynomial.Cardinal
Mathlib.Data.MvPolynomial.Comap
Mathlib.Data.MvPolynomial.CommRing
Mathlib.Data.MvPolynomial.Counit
Mathlib.Data.MvPolynomial.Division
Mathlib.Data.MvPolynomial.Equiv
Mathlib.Data.MvPolynomial.Invertible
Mathlib.Data.MvPolynomial.Rename
Mathlib.Data.MvPolynomial.Supported
Mathlib.Data.MvPolynomial.Variables
Mathlib.Data.Nat.Basic
Mathlib.Data.Nat.Bits
Mathlib.Data.Nat.Bitwise
Mathlib.Data.Nat.Count
Mathlib.Data.Nat.Digits
Mathlib.Data.Nat.Dist
Mathlib.Data.Nat.EvenOddRec
Mathlib.Data.Nat.Factors
Mathlib.Data.Nat.Fib
Mathlib.Data.Nat.ForSqrt
Mathlib.Data.Nat.Hyperoperation
Mathlib.Data.Nat.Interval
Mathlib.Data.Nat.Lattice
Mathlib.Data.Nat.Log
Mathlib.Data.Nat.ModEq
Mathlib.Data.Nat.Multiplicity
Mathlib.Data.Nat.PSub
Mathlib.Data.Nat.Pairing
Mathlib.Data.Nat.Parity
Mathlib.Data.Nat.PartENat
Mathlib.Data.Nat.Periodic
Mathlib.Data.Nat.Pow
Mathlib.Data.Nat.Prime
Mathlib.Data.Nat.PrimeFin
Mathlib.Data.Nat.Set
Mathlib.Data.Nat.Size
Mathlib.Data.Nat.Sqrt
Mathlib.Data.Nat.SuccPred
Mathlib.Data.Nat.Totient
Mathlib.Data.Nat.Units
Mathlib.Data.Nat.Upto
Mathlib.Data.Nat.WithBot
Mathlib.Data.Num.Basic
Mathlib.Data.Num.Bitwise
Mathlib.Data.Option.Basic
Mathlib.Data.Option.Defs
Mathlib.Data.Option.NAry
Mathlib.Data.PNat.Basic
Mathlib.Data.PNat.Defs
Mathlib.Data.PNat.Factors
Mathlib.Data.PNat.Find
Mathlib.Data.PNat.Interval
Mathlib.Data.PNat.Prime
Mathlib.Data.PNat.Xgcd
Mathlib.Data.PSigma.Order
Mathlib.Data.Pi.Algebra
Mathlib.Data.Pi.Interval
Mathlib.Data.Pi.Lex
Mathlib.Data.Polynomial.AlgebraMap
Mathlib.Data.Polynomial.Basic
Mathlib.Data.Polynomial.CancelLeads
Mathlib.Data.Polynomial.Cardinal
Mathlib.Data.Polynomial.Coeff
Mathlib.Data.Polynomial.DenomsClearable
Mathlib.Data.Polynomial.Derivative
Mathlib.Data.Polynomial.Div
Mathlib.Data.Polynomial.EraseLead
Mathlib.Data.Polynomial.Eval
Mathlib.Data.Polynomial.FieldDivision
Mathlib.Data.Polynomial.HasseDeriv
Mathlib.Data.Polynomial.Identities
Mathlib.Data.Polynomial.Induction
Mathlib.Data.Polynomial.Inductions
Mathlib.Data.Polynomial.IntegralNormalization
Mathlib.Data.Polynomial.Lifts
Mathlib.Data.Polynomial.Mirror
Mathlib.Data.Polynomial.Monic
Mathlib.Data.Polynomial.Monomial
Mathlib.Data.Polynomial.PartialFractions
Mathlib.Data.Polynomial.Reverse
Mathlib.Data.Polynomial.RingDivision
Mathlib.Data.Polynomial.Splits
Mathlib.Data.Polynomial.Taylor
Mathlib.Data.Prod.Basic
Mathlib.Data.Prod.Lex
Mathlib.Data.Prod.PProd
Mathlib.Data.Prod.TProd
Mathlib.Data.Rat.Basic
Mathlib.Data.Rat.BigOperators
Mathlib.Data.Rat.Cast
Mathlib.Data.Rat.Defs
Mathlib.Data.Rat.Denumerable
Mathlib.Data.Rat.Encodable
Mathlib.Data.Rat.Floor
Mathlib.Data.Rat.Init
Mathlib.Data.Rat.Lemmas
Mathlib.Data.Rat.NNRat
Mathlib.Data.Rat.Order
Mathlib.Data.Rat.Sqrt
Mathlib.Data.Real.Basic
Mathlib.Data.Real.CauSeq
Mathlib.Data.Real.CauSeqCompletion
Mathlib.Data.Real.ConjugateExponents
Mathlib.Data.Real.ENNReal
Mathlib.Data.Real.ENatENNReal
Mathlib.Data.Real.EReal
Mathlib.Data.Real.NNReal
Mathlib.Data.Real.Pointwise
Mathlib.Data.Real.Sign
Mathlib.Data.Real.Sqrt
Mathlib.Data.Seq.Computation
Mathlib.Data.Set.Accumulate
Mathlib.Data.Set.Basic
Mathlib.Data.Set.BoolIndicator
Mathlib.Data.Set.Constructions
Mathlib.Data.Set.Countable
Mathlib.Data.Set.Enumerate
Mathlib.Data.Set.Equitable
Mathlib.Data.Set.Finite
Mathlib.Data.Set.Function
Mathlib.Data.Set.Functor
Mathlib.Data.Set.Image
Mathlib.Data.Set.Lattice
Mathlib.Data.Set.MulAntidiagonal
Mathlib.Data.Set.NAry
Mathlib.Data.Set.Opposite
Mathlib.Data.Set.Prod
Mathlib.Data.Set.Semiring
Mathlib.Data.Set.Sigma
Mathlib.Data.Set.Sups
Mathlib.Data.Set.UnionLift
Mathlib.Data.SetLike.Basic
Mathlib.Data.SetLike.Fintype
Mathlib.Data.Setoid.Basic
Mathlib.Data.Setoid.Partition
Mathlib.Data.Sigma.Basic
Mathlib.Data.Sigma.Interval
Mathlib.Data.Sigma.Lex
Mathlib.Data.Sigma.Order
Mathlib.Data.Stream.Defs
Mathlib.Data.Stream.Init
Mathlib.Data.String.Defs
Mathlib.Data.String.Lemmas
Mathlib.Data.Sum.Basic
Mathlib.Data.Sum.Interval
Mathlib.Data.Sum.Order
Mathlib.Data.Sym.Basic
Mathlib.Data.Sym.Sym2
Mathlib.Data.TypeVec.Attr
Mathlib.Data.Vector.Basic
Mathlib.Data.Vector.Mem
Mathlib.Data.Vector.Zip
Mathlib.Data.W.Basic
Mathlib.Data.W.Cardinal
Mathlib.Data.W.Constructions
Mathlib.Data.ZMod.Algebra
Mathlib.Data.ZMod.Basic
Mathlib.Data.ZMod.Coprime
Mathlib.Data.ZMod.Defs
Mathlib.Data.ZMod.Parity
Mathlib.Dynamics.FixedPoints.Basic
Mathlib.Dynamics.FixedPoints.Topology
Mathlib.GroupTheory.GroupAction.Basic
Mathlib.GroupTheory.GroupAction.BigOperators
Mathlib.GroupTheory.GroupAction.ConjAct
Mathlib.GroupTheory.GroupAction.Defs
Mathlib.GroupTheory.GroupAction.Embedding
Mathlib.GroupTheory.GroupAction.FixingSubgroup
Mathlib.GroupTheory.GroupAction.Group
Mathlib.GroupTheory.GroupAction.Opposite
Mathlib.GroupTheory.GroupAction.Option
Mathlib.GroupTheory.GroupAction.Pi
Mathlib.GroupTheory.GroupAction.Prod
Mathlib.GroupTheory.GroupAction.Quotient
Mathlib.GroupTheory.GroupAction.Sigma
Mathlib.GroupTheory.GroupAction.SubMulAction
Mathlib.GroupTheory.GroupAction.Sum
Mathlib.GroupTheory.GroupAction.Support
Mathlib.GroupTheory.GroupAction.Units
Mathlib.GroupTheory.Perm.Basic
Mathlib.GroupTheory.Perm.List
Mathlib.GroupTheory.Perm.Option
Mathlib.GroupTheory.Perm.Sign
Mathlib.GroupTheory.Perm.Subgroup
Mathlib.GroupTheory.Perm.Support
Mathlib.GroupTheory.Perm.ViaEmbedding
Mathlib.GroupTheory.Subgroup.Actions
Mathlib.GroupTheory.Subgroup.Basic
Mathlib.GroupTheory.Subgroup.Finite
Mathlib.GroupTheory.Subgroup.MulOpposite
Mathlib.GroupTheory.Subgroup.Pointwise
Mathlib.GroupTheory.Subgroup.Saturated
Mathlib.GroupTheory.Subgroup.Simple
Mathlib.GroupTheory.Subgroup.Zpowers
Mathlib.GroupTheory.Submonoid.Basic
Mathlib.GroupTheory.Submonoid.Center
Mathlib.GroupTheory.Submonoid.Centralizer
Mathlib.GroupTheory.Submonoid.Inverses
Mathlib.GroupTheory.Submonoid.Membership
Mathlib.GroupTheory.Submonoid.Operations
Mathlib.GroupTheory.Submonoid.Pointwise
Mathlib.GroupTheory.Subsemigroup.Basic
Mathlib.GroupTheory.Subsemigroup.Center
Mathlib.GroupTheory.Subsemigroup.Centralizer
Mathlib.GroupTheory.Subsemigroup.Membership
Mathlib.GroupTheory.Subsemigroup.Operations
Mathlib.Init.Algebra.Classes
Mathlib.Init.Algebra.Functions
Mathlib.Init.Algebra.Order
Mathlib.Init.Classes.Order
Mathlib.Init.Control.Combinators
Mathlib.Init.Data.Prod
Mathlib.Init.Data.Quot
Mathlib.Init.Meta.WellFoundedTactics
Mathlib.Lean.Expr.Basic
Mathlib.Lean.Expr.ReplaceRec
Mathlib.Lean.Expr.Traverse
Mathlib.Lean.Meta.Simp
Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Mathlib.LinearAlgebra.AffineSpace.AffineMap
Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
Mathlib.LinearAlgebra.AffineSpace.Basic
Mathlib.LinearAlgebra.AffineSpace.Midpoint
Mathlib.LinearAlgebra.AffineSpace.MidpointZero
Mathlib.LinearAlgebra.AffineSpace.Ordered
Mathlib.LinearAlgebra.AffineSpace.Pointwise
Mathlib.LinearAlgebra.AffineSpace.Restrict
Mathlib.LinearAlgebra.AffineSpace.Slope
Mathlib.LinearAlgebra.Basis.Bilinear
Mathlib.Logic.Embedding.Basic
Mathlib.Logic.Embedding.Set
Mathlib.Logic.Encodable.Basic
Mathlib.Logic.Encodable.Lattice
Mathlib.Logic.Equiv.Basic
Mathlib.Logic.Equiv.Defs
Mathlib.Logic.Equiv.Embedding
Mathlib.Logic.Equiv.Fin
Mathlib.Logic.Equiv.Fintype
Mathlib.Logic.Equiv.Functor
Mathlib.Logic.Equiv.List
Mathlib.Logic.Equiv.LocalEquiv
Mathlib.Logic.Equiv.MfldSimpsAttr
Mathlib.Logic.Equiv.Nat
Mathlib.Logic.Equiv.Option
Mathlib.Logic.Equiv.Set
Mathlib.Logic.Function.Basic
Mathlib.Logic.Function.Conjugate
Mathlib.Logic.Function.Iterate
Mathlib.Logic.Small.Basic
Mathlib.Logic.Small.List
Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
Mathlib.NumberTheory.Padics.PadicNorm
Mathlib.NumberTheory.Padics.PadicVal
Mathlib.NumberTheory.Zsqrtd.Basic
Mathlib.NumberTheory.Zsqrtd.ToReal
Mathlib.Order.Atoms.Finite
Mathlib.Order.Bounds.Basic
Mathlib.Order.Bounds.OrderIso
Mathlib.Order.ConditionallyCompleteLattice.Basic
Mathlib.Order.ConditionallyCompleteLattice.Finset
Mathlib.Order.ConditionallyCompleteLattice.Group
Mathlib.Order.Extension.Linear
Mathlib.Order.Extension.Well
Mathlib.Order.Filter.Archimedean
Mathlib.Order.Filter.AtTopBot
Mathlib.Order.Filter.Bases
Mathlib.Order.Filter.Basic
Mathlib.Order.Filter.Cofinite
Mathlib.Order.Filter.CountableInter
Mathlib.Order.Filter.Curry
Mathlib.Order.Filter.ENNReal
Mathlib.Order.Filter.Extr
Mathlib.Order.Filter.FilterProduct
Mathlib.Order.Filter.Germ
Mathlib.Order.Filter.IndicatorFunction
Mathlib.Order.Filter.Interval
Mathlib.Order.Filter.Lift
Mathlib.Order.Filter.ModEq
Mathlib.Order.Filter.NAry
Mathlib.Order.Filter.Partial
Mathlib.Order.Filter.Pi
Mathlib.Order.Filter.Pointwise
Mathlib.Order.Filter.Prod
Mathlib.Order.Filter.SmallSets
Mathlib.Order.Filter.Ultrafilter
Mathlib.Order.Heyting.Basic
Mathlib.Order.Heyting.Boundary
Mathlib.Order.Heyting.Hom
Mathlib.Order.Heyting.Regular
Mathlib.Order.Hom.Basic
Mathlib.Order.Hom.Bounded
Mathlib.Order.Hom.CompleteLattice
Mathlib.Order.Hom.Lattice
Mathlib.Order.Hom.Order
Mathlib.Order.Hom.Set
Mathlib.Order.Monotone.Basic
Mathlib.Order.Monotone.Extension
Mathlib.Order.Monotone.Monovary
Mathlib.Order.Monotone.Odd
Mathlib.Order.Monotone.Union
Mathlib.Order.Partition.Equipartition
Mathlib.Order.Partition.Finpartition
Mathlib.Order.RelIso.Basic
Mathlib.Order.RelIso.Group
Mathlib.Order.RelIso.Set
Mathlib.Order.SuccPred.Basic
Mathlib.Order.SuccPred.IntervalSucc
Mathlib.Order.SuccPred.Limit
Mathlib.Order.SuccPred.LinearLocallyFinite
Mathlib.Order.SuccPred.Relation
Mathlib.Order.UpperLower.Basic
Mathlib.Order.UpperLower.Hom
Mathlib.Order.UpperLower.LocallyFinite
Mathlib.RingTheory.Adjoin.Basic
Mathlib.RingTheory.Coprime.Basic
Mathlib.RingTheory.Coprime.Ideal
Mathlib.RingTheory.Coprime.Lemmas
Mathlib.RingTheory.Ideal.Basic
Mathlib.RingTheory.Ideal.IdempotentFg
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Prod
Mathlib.RingTheory.Ideal.Quotient
Mathlib.RingTheory.Int.Basic
Mathlib.RingTheory.Localization.Basic
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.Localization.Integer
Mathlib.RingTheory.Localization.Module
Mathlib.RingTheory.Localization.NumDen
Mathlib.RingTheory.MvPolynomial.Symmetric
Mathlib.RingTheory.MvPolynomial.Tower
Mathlib.RingTheory.OreLocalization.Basic
Mathlib.RingTheory.OreLocalization.OreSet
Mathlib.RingTheory.Polynomial.Basic
Mathlib.RingTheory.Polynomial.Chebyshev
Mathlib.RingTheory.Polynomial.Content
Mathlib.RingTheory.Polynomial.Opposites
Mathlib.RingTheory.Polynomial.Pochhammer
Mathlib.RingTheory.Polynomial.ScaleRoots
Mathlib.RingTheory.Polynomial.Tower
Mathlib.RingTheory.Polynomial.Vieta
Mathlib.RingTheory.Subring.Basic
Mathlib.RingTheory.Subring.Pointwise
Mathlib.RingTheory.Subsemiring.Basic
Mathlib.RingTheory.Subsemiring.Pointwise
Mathlib.RingTheory.Valuation.Basic
Mathlib.RingTheory.Valuation.Integers
Mathlib.SetTheory.Cardinal.Basic
Mathlib.SetTheory.Cardinal.Cofinality
Mathlib.SetTheory.Cardinal.Continuum
Mathlib.SetTheory.Cardinal.Divisibility
Mathlib.SetTheory.Cardinal.Finite
Mathlib.SetTheory.Cardinal.Ordinal
Mathlib.SetTheory.Cardinal.SchroederBernstein
Mathlib.SetTheory.Ordinal.Arithmetic
Mathlib.SetTheory.Ordinal.Basic
Mathlib.SetTheory.Ordinal.CantorNormalForm
Mathlib.SetTheory.Ordinal.Exponential
Mathlib.SetTheory.Ordinal.FixedPoint
Mathlib.SetTheory.Ordinal.NaturalOps
Mathlib.SetTheory.Ordinal.Principal
Mathlib.SetTheory.Ordinal.Topology
Mathlib.Tactic.Continuity.Init
Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Elimination
Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.Parsing
Mathlib.Tactic.Linarith.Preprocessing
Mathlib.Tactic.Linarith.Verification
Mathlib.Tactic.Monotonicity.Attr
Mathlib.Tactic.Monotonicity.Basic
Mathlib.Tactic.Monotonicity.Lemmas
Mathlib.Tactic.Nontriviality.Core
Mathlib.Tactic.NormCast.Tactic
Mathlib.Tactic.NormNum.Basic
Mathlib.Tactic.NormNum.Core
Mathlib.Tactic.Positivity.Basic
Mathlib.Tactic.Positivity.Core
Mathlib.Tactic.Qify.Attr
Mathlib.Tactic.Relation.Rfl
Mathlib.Tactic.Relation.Symm
Mathlib.Tactic.Relation.Trans
Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Simps.Basic
Mathlib.Tactic.Simps.NotationClass
Mathlib.Tactic.Zify.Attr
Mathlib.Testing.SlimCheck.Gen
Mathlib.Testing.SlimCheck.Sampleable
Mathlib.Testing.SlimCheck.Testable
Mathlib.Topology.Algebra.Affine
Mathlib.Topology.Algebra.ConstMulAction
Mathlib.Topology.Algebra.Constructions
Mathlib.Topology.Algebra.Field
Mathlib.Topology.Algebra.GroupCompletion
Mathlib.Topology.Algebra.GroupWithZero
Mathlib.Topology.Algebra.Localization
Mathlib.Topology.Algebra.Monoid
Mathlib.Topology.Algebra.MulAction
Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Topology.Algebra.Polynomial
Mathlib.Topology.Algebra.Semigroup
Mathlib.Topology.Algebra.Star
Mathlib.Topology.Algebra.UniformGroup
Mathlib.Topology.Algebra.UniformMulAction
Mathlib.Topology.Algebra.UniformRing
Mathlib.Topology.Algebra.WithZeroTopology
Mathlib.Topology.Bornology.Basic
Mathlib.Topology.Bornology.Constructions
Mathlib.Topology.Bornology.Hom
Mathlib.Topology.Category.Born
Mathlib.Topology.ContinuousFunction.Basic
Mathlib.Topology.ContinuousFunction.CocompactMap
Mathlib.Topology.ContinuousFunction.Ordered
Mathlib.Topology.ContinuousFunction.T0Sierpinski
Mathlib.Topology.FiberBundle.Basic
Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Mathlib.Topology.FiberBundle.Trivialization
Mathlib.Topology.Hom.Open
Mathlib.Topology.Homotopy.Basic
Mathlib.Topology.Homotopy.Equiv
Mathlib.Topology.Instances.ENNReal
Mathlib.Topology.Instances.EReal
Mathlib.Topology.Instances.Int
Mathlib.Topology.Instances.NNReal
Mathlib.Topology.Instances.Nat
Mathlib.Topology.Instances.Rat
Mathlib.Topology.Instances.Real
Mathlib.Topology.Instances.Sign
Mathlib.Topology.LocallyConstant.Algebra
Mathlib.Topology.LocallyConstant.Basic
Mathlib.Topology.MetricSpace.Algebra
Mathlib.Topology.MetricSpace.Antilipschitz
Mathlib.Topology.MetricSpace.Basic
Mathlib.Topology.MetricSpace.CauSeqFilter
Mathlib.Topology.MetricSpace.Completion
Mathlib.Topology.MetricSpace.EMetricParacompact
Mathlib.Topology.MetricSpace.EMetricSpace
Mathlib.Topology.MetricSpace.Equicontinuity
Mathlib.Topology.MetricSpace.Gluing
Mathlib.Topology.MetricSpace.Infsep
Mathlib.Topology.MetricSpace.IsometricSMul
Mathlib.Topology.MetricSpace.Isometry
Mathlib.Topology.MetricSpace.Lipschitz
Mathlib.Topology.MetricSpace.MetricSeparated
Mathlib.Topology.MetricSpace.ShrinkingLemma
Mathlib.Topology.Order.Basic
Mathlib.Topology.Order.Lattice
Mathlib.Topology.Order.LowerTopology
Mathlib.Topology.Order.Priestley
Mathlib.Topology.Sets.Closeds
Mathlib.Topology.Sets.Compacts
Mathlib.Topology.Sets.Opens
Mathlib.Topology.Sets.Order
Mathlib.Topology.Spectral.Hom
Mathlib.Topology.UniformSpace.AbsoluteValue
Mathlib.Topology.UniformSpace.AbstractCompletion
Mathlib.Topology.UniformSpace.Basic
Mathlib.Topology.UniformSpace.Cauchy
Mathlib.Topology.UniformSpace.Compact
Mathlib.Topology.UniformSpace.CompactConvergence
Mathlib.Topology.UniformSpace.CompareReals
Mathlib.Topology.UniformSpace.CompleteSeparated
Mathlib.Topology.UniformSpace.Completion
Mathlib.Topology.UniformSpace.Equicontinuity
Mathlib.Topology.UniformSpace.Equiv
Mathlib.Topology.UniformSpace.Pi
Mathlib.Topology.UniformSpace.Separation
Mathlib.Topology.UniformSpace.UniformConvergence
Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Mathlib.Topology.UniformSpace.UniformEmbedding
Mathlib.Algebra.Algebra.Subalgebra.Basic
Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Mathlib.Algebra.Algebra.Subalgebra.Tower
Mathlib.Algebra.BigOperators.Multiset.Basic
Mathlib.Algebra.BigOperators.Multiset.Lemmas
Mathlib.Algebra.Category.GroupCat.Basic
Mathlib.Algebra.Category.GroupCat.Preadditive
Mathlib.Algebra.Category.GroupCat.Zero
Mathlib.Algebra.Category.MonCat.Basic
Mathlib.Algebra.Group.WithOne.Basic
Mathlib.Algebra.Group.WithOne.Defs
Mathlib.Algebra.Group.WithOne.Units
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Algebra.GroupWithZero.Units.Lemmas
Mathlib.Algebra.Hom.Equiv.Basic
Mathlib.Algebra.Hom.Equiv.TypeTags
Mathlib.Algebra.Module.Submodule.Basic
Mathlib.Algebra.Module.Submodule.Bilinear
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.Algebra.Module.Submodule.Pointwise
Mathlib.Algebra.Order.Field.Basic
Mathlib.Algebra.Order.Field.Defs
Mathlib.Algebra.Order.Field.InjSurj
Mathlib.Algebra.Order.Field.Pi
Mathlib.Algebra.Order.Field.Power
Mathlib.Algebra.Order.Group.Abs
Mathlib.Algebra.Order.Group.Bounds
Mathlib.Algebra.Order.Group.Defs
Mathlib.Algebra.Order.Group.DenselyOrdered
Mathlib.Algebra.Order.Group.InjSurj
Mathlib.Algebra.Order.Group.Instances
Mathlib.Algebra.Order.Group.MinMax
Mathlib.Algebra.Order.Group.OrderIso
Mathlib.Algebra.Order.Group.Prod
Mathlib.Algebra.Order.Group.TypeTags
Mathlib.Algebra.Order.Group.Units
Mathlib.Algebra.Order.Group.WithTop
Mathlib.Algebra.Order.Hom.Basic
Mathlib.Algebra.Order.Hom.Monoid
Mathlib.Algebra.Order.Hom.Ring
Mathlib.Algebra.Order.Monoid.Basic
Mathlib.Algebra.Order.Monoid.Defs
Mathlib.Algebra.Order.Monoid.Lemmas
Mathlib.Algebra.Order.Monoid.MinMax
Mathlib.Algebra.Order.Monoid.NatCast
Mathlib.Algebra.Order.Monoid.OrderDual
Mathlib.Algebra.Order.Monoid.Prod
Mathlib.Algebra.Order.Monoid.ToMulBot
Mathlib.Algebra.Order.Monoid.TypeTags
Mathlib.Algebra.Order.Monoid.Units
Mathlib.Algebra.Order.Monoid.WithTop
Mathlib.Algebra.Order.Nonneg.Field
Mathlib.Algebra.Order.Nonneg.Floor
Mathlib.Algebra.Order.Nonneg.Ring
Mathlib.Algebra.Order.Positive.Field
Mathlib.Algebra.Order.Positive.Ring
Mathlib.Algebra.Order.Ring.Abs
Mathlib.Algebra.Order.Ring.Canonical
Mathlib.Algebra.Order.Ring.CharZero
Mathlib.Algebra.Order.Ring.Cone
Mathlib.Algebra.Order.Ring.Defs
Mathlib.Algebra.Order.Ring.InjSurj
Mathlib.Algebra.Order.Ring.Lemmas
Mathlib.Algebra.Order.Ring.WithTop
Mathlib.Algebra.Order.Sub.Basic
Mathlib.Algebra.Order.Sub.Canonical
Mathlib.Algebra.Order.Sub.Defs
Mathlib.Algebra.Order.Sub.WithTop
Mathlib.Analysis.Normed.Field.Basic
Mathlib.Analysis.Normed.Field.InfiniteSum
Mathlib.Analysis.Normed.Field.UnitBall
Mathlib.Analysis.Normed.Group.BallSphere
Mathlib.Analysis.Normed.Group.Basic
Mathlib.Analysis.Normed.Group.Completion
Mathlib.Analysis.Normed.Group.Hom
Mathlib.Analysis.Normed.Group.HomCompletion
Mathlib.Analysis.Normed.Group.InfiniteSum
Mathlib.Analysis.Normed.Group.Seminorm
Mathlib.Analysis.Normed.Order.Lattice
Mathlib.CategoryTheory.Category.Cat.Limit
Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Mathlib.CategoryTheory.Limits.Constructions.Filtered
Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Mathlib.CategoryTheory.Limits.Preserves.Basic
Mathlib.CategoryTheory.Limits.Preserves.Filtered
Mathlib.CategoryTheory.Limits.Preserves.Finite
Mathlib.CategoryTheory.Limits.Preserves.Limits
Mathlib.CategoryTheory.Limits.Preserves.Opposites
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Mathlib.CategoryTheory.Limits.Shapes.CommSq
Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Mathlib.CategoryTheory.Limits.Shapes.Equivalence
Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
Mathlib.CategoryTheory.Limits.Shapes.FunctorCategory
Mathlib.CategoryTheory.Limits.Shapes.Images
Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Mathlib.CategoryTheory.Limits.Shapes.Kernels
Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Mathlib.CategoryTheory.Limits.Shapes.Products
Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Mathlib.CategoryTheory.Limits.Shapes.Terminal
Mathlib.CategoryTheory.Limits.Shapes.Types
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Mathlib.Combinatorics.SetFamily.Compression.Down
Mathlib.Combinatorics.SetFamily.Compression.UV
Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Mathlib.Data.Fin.Tuple.Basic
Mathlib.Data.Fin.Tuple.BubbleSortInduction
Mathlib.Data.Fin.Tuple.Monotone
Mathlib.Data.Fin.Tuple.NatAntidiagonal
Mathlib.Data.Fin.Tuple.Sort
Mathlib.Data.Int.Cast.Basic
Mathlib.Data.Int.Cast.Defs
Mathlib.Data.Int.Cast.Field
Mathlib.Data.Int.Cast.Lemmas
Mathlib.Data.Int.Cast.Prod
Mathlib.Data.Int.Dvd.Basic
Mathlib.Data.Int.Dvd.Pow
Mathlib.Data.Int.Order.Basic
Mathlib.Data.Int.Order.Lemmas
Mathlib.Data.Int.Order.Units
Mathlib.Data.List.BigOperators.Basic
Mathlib.Data.List.BigOperators.Lemmas
Mathlib.Data.Nat.Cast.Basic
Mathlib.Data.Nat.Cast.Defs
Mathlib.Data.Nat.Cast.Field
Mathlib.Data.Nat.Cast.Prod
Mathlib.Data.Nat.Cast.WithTop
Mathlib.Data.Nat.Choose.Basic
Mathlib.Data.Nat.Choose.Bounds
Mathlib.Data.Nat.Choose.Cast
Mathlib.Data.Nat.Choose.Central
Mathlib.Data.Nat.Choose.Dvd
Mathlib.Data.Nat.Choose.Factorization
Mathlib.Data.Nat.Choose.Sum
Mathlib.Data.Nat.Choose.Vandermonde
Mathlib.Data.Nat.Factorial.Basic
Mathlib.Data.Nat.Factorial.BigOperators
Mathlib.Data.Nat.Factorial.Cast
Mathlib.Data.Nat.Factorization.Basic
Mathlib.Data.Nat.Factorization.PrimePow
Mathlib.Data.Nat.GCD.Basic
Mathlib.Data.Nat.GCD.BigOperators
Mathlib.Data.Nat.Order.Basic
Mathlib.Data.Nat.Order.Lemmas
Mathlib.Data.PFunctor.Multivariate.Basic
Mathlib.Data.PFunctor.Multivariate.M
Mathlib.Data.PFunctor.Multivariate.W
Mathlib.Data.PFunctor.Univariate.Basic
Mathlib.Data.PFunctor.Univariate.M
Mathlib.Data.Polynomial.Degree.CardPowDegree
Mathlib.Data.Polynomial.Degree.Definitions
Mathlib.Data.Polynomial.Degree.Lemmas
Mathlib.Data.Polynomial.Degree.TrailingDegree
Mathlib.Data.QPF.Multivariate.Basic
Mathlib.Data.Set.Intervals.Basic
Mathlib.Data.Set.Intervals.Disjoint
Mathlib.Data.Set.Intervals.Group
Mathlib.Data.Set.Intervals.Infinite
Mathlib.Data.Set.Intervals.Instances
Mathlib.Data.Set.Intervals.IsoIoo
Mathlib.Data.Set.Intervals.Monoid
Mathlib.Data.Set.Intervals.Monotone
Mathlib.Data.Set.Intervals.OrdConnected
Mathlib.Data.Set.Intervals.OrdConnectedComponent
Mathlib.Data.Set.Intervals.OrderIso
Mathlib.Data.Set.Intervals.Pi
Mathlib.Data.Set.Intervals.ProjIcc
Mathlib.Data.Set.Intervals.SurjOn
Mathlib.Data.Set.Intervals.UnorderedInterval
Mathlib.Data.Set.Intervals.WithBotTop
Mathlib.Data.Set.Pairwise.Basic
Mathlib.Data.Set.Pairwise.Lattice
Mathlib.Data.Set.Pointwise.Basic
Mathlib.Data.Set.Pointwise.BigOperators
Mathlib.Data.Set.Pointwise.Finite
Mathlib.Data.Set.Pointwise.Interval
Mathlib.Data.Set.Pointwise.Iterate
Mathlib.Data.Set.Pointwise.ListOfFn
Mathlib.Data.Set.Pointwise.SMul
Mathlib.Data.Set.Pointwise.Support
Mathlib.Data.Sym.Sym2.Init
Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Mathlib.GroupTheory.Perm.Cycle.Basic
Mathlib.Init.Data.Bool.Basic
Mathlib.Init.Data.Bool.Lemmas
Mathlib.Init.Data.Fin.Basic
Mathlib.Init.Data.Int.Basic
Mathlib.Init.Data.Int.Bitwise
Mathlib.Init.Data.Int.DivMod
Mathlib.Init.Data.Int.Lemmas
Mathlib.Init.Data.Int.Order
Mathlib.Init.Data.List.Basic
Mathlib.Init.Data.List.Instances
Mathlib.Init.Data.List.Lemmas
Mathlib.Init.Data.Nat.Basic
Mathlib.Init.Data.Nat.Bitwise
Mathlib.Init.Data.Nat.Div
Mathlib.Init.Data.Nat.GCD
Mathlib.Init.Data.Nat.Lemmas
Mathlib.Init.Data.Nat.Notation
Mathlib.Init.Data.Option.Basic
Mathlib.Init.Data.Option.Lemmas
Mathlib.Init.Data.Ordering.Basic
Mathlib.Init.Data.Rat.Basic
Mathlib.Init.Data.Sigma.Basic
Mathlib.Init.Data.Subtype.Basic
Mathlib.Topology.Algebra.Group.Basic
Mathlib.Topology.Algebra.Group.Compact
Mathlib.Topology.Algebra.InfiniteSum.Basic
Mathlib.Topology.Algebra.InfiniteSum.Order
Mathlib.Topology.Algebra.InfiniteSum.Real
Mathlib.Topology.Algebra.InfiniteSum.Ring
Mathlib.Topology.Algebra.Nonarchimedean.Basic
Mathlib.Topology.Algebra.Order.Archimedean
Mathlib.Topology.Algebra.Order.Compact
Mathlib.Topology.Algebra.Order.ExtendFrom
Mathlib.Topology.Algebra.Order.ExtrClosure
Mathlib.Topology.Algebra.Order.Field
Mathlib.Topology.Algebra.Order.Filter
Mathlib.Topology.Algebra.Order.Floor
Mathlib.Topology.Algebra.Order.Group
Mathlib.Topology.Algebra.Order.IntermediateValue
Mathlib.Topology.Algebra.Order.LeftRight
Mathlib.Topology.Algebra.Order.LeftRightLim
Mathlib.Topology.Algebra.Order.LiminfLimsup
Mathlib.Topology.Algebra.Order.MonotoneContinuity
Mathlib.Topology.Algebra.Order.MonotoneConvergence
Mathlib.Topology.Algebra.Order.ProjIcc
Mathlib.Topology.Algebra.Order.T5
Mathlib.Topology.Algebra.Order.UpperLower
Mathlib.Topology.Algebra.Ring.Basic
Mathlib.Topology.Algebra.Ring.Ideal
Mathlib.Topology.Order.Hom.Basic
Mathlib.Algebra.Hom.Equiv.Units.Basic
Mathlib.Algebra.Hom.Equiv.Units.GroupWithZero
Mathlib.Algebra.Order.Field.Canonical.Basic
Mathlib.Algebra.Order.Field.Canonical.Defs
Mathlib.Algebra.Order.Monoid.Cancel.Basic
Mathlib.Algebra.Order.Monoid.Cancel.Defs
Mathlib.Algebra.Order.Monoid.Canonical.Defs
Mathlib.Algebra.Order.Monoid.WithZero.Basic
Mathlib.Algebra.Order.Monoid.WithZero.Defs
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Mathlib.Data.QPF.Multivariate.Constructions.Comp
Mathlib.Data.QPF.Multivariate.Constructions.Const
Mathlib.Data.QPF.Multivariate.Constructions.Fix
Mathlib.Data.QPF.Multivariate.Constructions.Prj
Mathlib.Data.QPF.Multivariate.Constructions.Quot
Mathlib.Data.QPF.Multivariate.Constructions.Sigma
Mathlib.Init.Data.Option.Init.Lemmas

Imported by