mathlib documentation

core / init.default

source

Imports

init.cc_lemmas
init.classical
init.coe
init.control.combinators
init.core
init.function
init.funext
init.logic
init.meta.float
init.meta.well_founded_tactics
init.propext
init.util
init.version
init.wf

Imported by

data.buffer
data.buffer.parser
data.dlist
data.stream
system.io
system.io_interface
system.random
algebra.absolute_value
algebra.add_torsor
algebra.algebra.basic
algebra.algebra.operations
algebra.algebra.ordered
algebra.algebra.restrict_scalars
algebra.algebra.subalgebra
algebra.algebra.tower
algebra.archimedean
algebra.associated
algebra.big_operators.basic
algebra.big_operators.enat
algebra.big_operators.fin
algebra.big_operators.finprod
algebra.big_operators.finsupp
algebra.big_operators.intervals
algebra.big_operators.nat_antidiagonal
algebra.big_operators.order
algebra.big_operators.pi
algebra.big_operators.ring
algebra.bounds
algebra.category.Algebra.basic
algebra.category.Algebra.limits
algebra.category.CommRing.adjunctions
algebra.category.CommRing.basic
algebra.category.CommRing.colimits
algebra.category.CommRing.limits
algebra.category.FinVect
algebra.category.Group.Z_Module_equivalence
algebra.category.Group.abelian
algebra.category.Group.adjunctions
algebra.category.Group.basic
algebra.category.Group.biproducts
algebra.category.Group.colimits
algebra.category.Group.images
algebra.category.Group.limits
algebra.category.Group.preadditive
algebra.category.Group.subobject
algebra.category.Group.zero
algebra.category.Module.abelian
algebra.category.Module.adjunctions
algebra.category.Module.basic
algebra.category.Module.colimits
algebra.category.Module.epi_mono
algebra.category.Module.kernels
algebra.category.Module.limits
algebra.category.Module.monoidal
algebra.category.Module.projective
algebra.category.Module.subobject
algebra.category.Mon.adjunctions
algebra.category.Mon.basic
algebra.category.Mon.colimits
algebra.category.Mon.limits
algebra.category.Semigroup.basic
algebra.char_p.algebra
algebra.char_p.basic
algebra.char_p.exp_char
algebra.char_p.invertible
algebra.char_p.pi
algebra.char_p.quotient
algebra.char_p.subring
algebra.char_zero
algebra.continued_fractions.basic
algebra.continued_fractions.computation.approximation_corollaries
algebra.continued_fractions.computation.approximations
algebra.continued_fractions.computation.basic
algebra.continued_fractions.computation.correctness_terminating
algebra.continued_fractions.computation.default
algebra.continued_fractions.computation.terminates_iff_rat
algebra.continued_fractions.computation.translations
algebra.continued_fractions.continuants_recurrence
algebra.continued_fractions.convergents_equiv
algebra.continued_fractions.default
algebra.continued_fractions.terminated_stable
algebra.continued_fractions.translations
algebra.covariant_and_contravariant
algebra.direct_limit
algebra.direct_sum.algebra
algebra.direct_sum.basic
algebra.direct_sum.finsupp
algebra.direct_sum.module
algebra.direct_sum.ring
algebra.divisibility
algebra.euclidean_absolute_value
algebra.euclidean_domain
algebra.field
algebra.field_power
algebra.floor
algebra.free
algebra.free_algebra
algebra.free_monoid
algebra.free_non_unital_non_assoc_algebra
algebra.gcd_monoid.basic
algebra.gcd_monoid.finset
algebra.gcd_monoid.multiset
algebra.geom_sum
algebra.group.basic
algebra.group.commute
algebra.group.conj
algebra.group.default
algebra.group.defs
algebra.group.hom
algebra.group.hom_instances
algebra.group.inj_surj
algebra.group.pi
algebra.group.prod
algebra.group.semiconj
algebra.group.to_additive
algebra.group.type_tags
algebra.group.ulift
algebra.group.units
algebra.group.units_hom
algebra.group.with_one
algebra.group_action_hom
algebra.group_power.basic
algebra.group_power.identities
algebra.group_power.lemmas
algebra.group_power.order
algebra.group_ring_action
algebra.group_with_zero.basic
algebra.group_with_zero.defs
algebra.group_with_zero.power
algebra.hierarchy_design
algebra.homology.additive
algebra.homology.augment
algebra.homology.complex_shape
algebra.homology.differential_object
algebra.homology.exact
algebra.homology.flip
algebra.homology.functor
algebra.homology.homological_complex
algebra.homology.homology
algebra.homology.homotopy
algebra.homology.homotopy_category
algebra.homology.image_to_kernel
algebra.homology.quasi_iso
algebra.homology.single
algebra.indicator_function
algebra.invertible
algebra.iterate_hom
algebra.lattice_ordered_group
algebra.lie.abelian
algebra.lie.base_change
algebra.lie.basic
algebra.lie.cartan_matrix
algebra.lie.cartan_subalgebra
algebra.lie.character
algebra.lie.classical
algebra.lie.direct_sum
algebra.lie.free
algebra.lie.ideal_operations
algebra.lie.matrix
algebra.lie.nilpotent
algebra.lie.non_unital_non_assoc_algebra
algebra.lie.of_associative
algebra.lie.quotient
algebra.lie.semisimple
algebra.lie.skew_adjoint
algebra.lie.solvable
algebra.lie.subalgebra
algebra.lie.submodule
algebra.lie.tensor_product
algebra.lie.universal_enveloping
algebra.lie.weights
algebra.linear_ordered_comm_group_with_zero
algebra.linear_recurrence
algebra.module.basic
algebra.module.default
algebra.module.hom
algebra.module.linear_map
algebra.module.opposites
algebra.module.ordered
algebra.module.pi
algebra.module.prod
algebra.module.projective
algebra.module.submodule
algebra.module.submodule_lattice
algebra.module.ulift
algebra.monoid_algebra.basic
algebra.monoid_algebra.to_direct_sum
algebra.non_unital_alg_hom
algebra.opposites
algebra.order
algebra.order_functions
algebra.ordered_field
algebra.ordered_group
algebra.ordered_monoid
algebra.ordered_monoid_lemmas
algebra.ordered_pi
algebra.ordered_pointwise
algebra.ordered_ring
algebra.ordered_smul
algebra.ordered_sub
algebra.pempty_instances
algebra.periodic
algebra.pointwise
algebra.polynomial.big_operators
algebra.polynomial.group_ring_action
algebra.punit_instances
algebra.quadratic_discriminant
algebra.quandle
algebra.quaternion
algebra.quaternion_basis
algebra.regular.basic
algebra.regular.pow
algebra.regular.smul
algebra.ring.basic
algebra.ring.boolean_ring
algebra.ring.default
algebra.ring.pi
algebra.ring.prod
algebra.ring.ulift
algebra.ring_quot
algebra.smul_with_zero
algebra.squarefree
algebra.star.algebra
algebra.star.basic
algebra.star.chsh
algebra.star.pi
algebra.support
algebra.triv_sq_zero_ext
algebra.tropical.basic
algebraic_geometry.EllipticCurve
algebraic_geometry.Scheme
algebraic_geometry.Spec
algebraic_geometry.is_open_comap_C
algebraic_geometry.locally_ringed_space
algebraic_geometry.presheafed_space
algebraic_geometry.presheafed_space.has_colimits
algebraic_geometry.prime_spectrum
algebraic_geometry.sheafed_space
algebraic_geometry.stalks
algebraic_geometry.structure_sheaf
algebraic_topology.Moore_complex
algebraic_topology.cech_nerve
algebraic_topology.simplex_category
algebraic_topology.simplicial_object
algebraic_topology.simplicial_set
algebraic_topology.topological_simplex
analysis.ODE.gronwall
analysis.analytic.basic
analysis.analytic.composition
analysis.analytic.inverse
analysis.analytic.linear
analysis.analytic.radius_liminf
analysis.asymptotics.asymptotic_equivalent
analysis.asymptotics.asymptotics
analysis.asymptotics.specific_asymptotics
analysis.calculus.conformal
analysis.calculus.darboux
analysis.calculus.deriv
analysis.calculus.extend_deriv
analysis.calculus.fderiv
analysis.calculus.fderiv_measurable
analysis.calculus.fderiv_symmetric
analysis.calculus.formal_multilinear_series
analysis.calculus.implicit
analysis.calculus.inverse
analysis.calculus.iterated_deriv
analysis.calculus.lagrange_multipliers
analysis.calculus.lhopital
analysis.calculus.local_extr
analysis.calculus.mean_value
analysis.calculus.parametric_integral
analysis.calculus.specific_functions
analysis.calculus.tangent_cone
analysis.calculus.times_cont_diff
analysis.complex.basic
analysis.complex.circle
analysis.complex.conformal
analysis.complex.isometry
analysis.complex.polynomial
analysis.complex.real_deriv
analysis.complex.roots_of_unity
analysis.complex.upper_half_plane
analysis.convex.basic
analysis.convex.caratheodory
analysis.convex.combination
analysis.convex.cone
analysis.convex.exposed
analysis.convex.extrema
analysis.convex.extreme
analysis.convex.independent
analysis.convex.integral
analysis.convex.specific_functions
analysis.convex.topology
analysis.fourier
analysis.hofer
analysis.mean_inequalities
analysis.normed_space.SemiNormedGroup
analysis.normed_space.SemiNormedGroup.kernels
analysis.normed_space.add_torsor
analysis.normed_space.affine_isometry
analysis.normed_space.banach
analysis.normed_space.basic
analysis.normed_space.bounded_linear_maps
analysis.normed_space.complemented
analysis.normed_space.conformal_linear_map
analysis.normed_space.dual
analysis.normed_space.enorm
analysis.normed_space.euclidean_dist
analysis.normed_space.exponential
analysis.normed_space.extend
analysis.normed_space.finite_dimension
analysis.normed_space.hahn_banach
analysis.normed_space.indicator_function
analysis.normed_space.inner_product
analysis.normed_space.int
analysis.normed_space.linear_isometry
analysis.normed_space.mazur_ulam
analysis.normed_space.multilinear
analysis.normed_space.normed_group_hom
analysis.normed_space.normed_group_hom_completion
analysis.normed_space.normed_group_quotient
analysis.normed_space.operator_norm
analysis.normed_space.ordered
analysis.normed_space.pi_Lp
analysis.normed_space.riesz_lemma
analysis.normed_space.units
analysis.normed_space.weak_dual
analysis.p_series
analysis.quaternion
analysis.seminorm
analysis.special_functions.arsinh
analysis.special_functions.bernstein
analysis.special_functions.exp_log
analysis.special_functions.integrals
analysis.special_functions.polynomials
analysis.special_functions.pow
analysis.special_functions.sqrt
analysis.special_functions.trigonometric
analysis.specific_limits
category_theory.Fintype
category_theory.abelian.basic
category_theory.abelian.diagram_lemmas.four
category_theory.abelian.exact
category_theory.abelian.ext
category_theory.abelian.non_preadditive
category_theory.abelian.opposite
category_theory.abelian.projective
category_theory.abelian.pseudoelements
category_theory.action
category_theory.additive.basic
category_theory.adjunction.adjoint_functor_theorems
category_theory.adjunction.basic
category_theory.adjunction.comma
category_theory.adjunction.fully_faithful
category_theory.adjunction.lifting
category_theory.adjunction.limits
category_theory.adjunction.mates
category_theory.adjunction.opposites
category_theory.adjunction.over
category_theory.adjunction.reflective
category_theory.arrow
category_theory.category.Cat
category_theory.category.Groupoid
category_theory.category.Kleisli
category_theory.category.Quiv
category_theory.category.Rel
category_theory.category.default
category_theory.category.pairwise
category_theory.category.preorder
category_theory.category.ulift
category_theory.closed.cartesian
category_theory.closed.functor
category_theory.closed.ideal
category_theory.closed.monoidal
category_theory.closed.types
category_theory.closed.zero
category_theory.comma
category_theory.concrete_category.basic
category_theory.concrete_category.bundled
category_theory.concrete_category.bundled_hom
category_theory.concrete_category.reflects_isomorphisms
category_theory.concrete_category.unbundled_hom
category_theory.conj
category_theory.connected_components
category_theory.const
category_theory.core
category_theory.currying
category_theory.derived
category_theory.differential_object
category_theory.discrete_category
category_theory.elements
category_theory.endomorphism
category_theory.enriched.basic
category_theory.epi_mono
category_theory.eq_to_hom
category_theory.equivalence
category_theory.essential_image
category_theory.essentially_small
category_theory.filtered
category_theory.fin_category
category_theory.full_subcategory
category_theory.fully_faithful
category_theory.functor
category_theory.functor_category
category_theory.functorial
category_theory.graded_object
category_theory.grothendieck
category_theory.groupoid
category_theory.hom_functor
category_theory.is_connected
category_theory.isomorphism
category_theory.isomorphism_classes
category_theory.lifting_properties
category_theory.limits.colimit_limit
category_theory.limits.comma
category_theory.limits.concrete_category
category_theory.limits.cones
category_theory.limits.connected
category_theory.limits.constructions.binary_products
category_theory.limits.constructions.epi_mono
category_theory.limits.constructions.equalizers
category_theory.limits.constructions.finite_products_of_binary_products
category_theory.limits.constructions.limits_of_products_and_equalizers
category_theory.limits.constructions.over.connected
category_theory.limits.constructions.over.default
category_theory.limits.constructions.over.products
category_theory.limits.constructions.pullbacks
category_theory.limits.constructions.weakly_initial
category_theory.limits.creates
category_theory.limits.filtered_colimit_commutes_finite_limit
category_theory.limits.final
category_theory.limits.fubini
category_theory.limits.functor_category
category_theory.limits.has_limits
category_theory.limits.is_limit
category_theory.limits.kan_extension
category_theory.limits.lattice
category_theory.limits.opposites
category_theory.limits.over
category_theory.limits.pi
category_theory.limits.preserves.basic
category_theory.limits.preserves.functor_category
category_theory.limits.preserves.limits
category_theory.limits.preserves.shapes.binary_products
category_theory.limits.preserves.shapes.equalizers
category_theory.limits.preserves.shapes.products
category_theory.limits.preserves.shapes.pullbacks
category_theory.limits.preserves.shapes.terminal
category_theory.limits.presheaf
category_theory.limits.punit
category_theory.limits.shapes.binary_products
category_theory.limits.shapes.biproducts
category_theory.limits.shapes.concrete_category
category_theory.limits.shapes.disjoint_coproduct
category_theory.limits.shapes.equalizers
category_theory.limits.shapes.finite_limits
category_theory.limits.shapes.finite_products
category_theory.limits.shapes.images
category_theory.limits.shapes.kernel_pair
category_theory.limits.shapes.kernels
category_theory.limits.shapes.normal_mono
category_theory.limits.shapes.products
category_theory.limits.shapes.pullbacks
category_theory.limits.shapes.reflexive
category_theory.limits.shapes.regular_mono
category_theory.limits.shapes.split_coequalizer
category_theory.limits.shapes.strict_initial
category_theory.limits.shapes.strong_epi
category_theory.limits.shapes.terminal
category_theory.limits.shapes.types
category_theory.limits.shapes.wide_equalizers
category_theory.limits.shapes.wide_pullbacks
category_theory.limits.shapes.zero
category_theory.limits.small_complete
category_theory.limits.types
category_theory.limits.yoneda
category_theory.linear.default
category_theory.linear.linear_functor
category_theory.linear.yoneda
category_theory.monad.adjunction
category_theory.monad.algebra
category_theory.monad.basic
category_theory.monad.coequalizer
category_theory.monad.equiv_mon
category_theory.monad.kleisli
category_theory.monad.limits
category_theory.monad.monadicity
category_theory.monad.products
category_theory.monad.types
category_theory.monoidal.CommMon_
category_theory.monoidal.End
category_theory.monoidal.Mod
category_theory.monoidal.Mon_
category_theory.monoidal.braided
category_theory.monoidal.category
category_theory.monoidal.center
category_theory.monoidal.discrete
category_theory.monoidal.free.basic
category_theory.monoidal.free.coherence
category_theory.monoidal.functor
category_theory.monoidal.functor_category
category_theory.monoidal.functorial
category_theory.monoidal.internal.Module
category_theory.monoidal.internal.functor_category
category_theory.monoidal.internal.limits
category_theory.monoidal.internal.types
category_theory.monoidal.limits
category_theory.monoidal.natural_transformation
category_theory.monoidal.of_chosen_finite_products
category_theory.monoidal.of_has_finite_products
category_theory.monoidal.opposite
category_theory.monoidal.preadditive
category_theory.monoidal.rigid
category_theory.monoidal.skeleton
category_theory.monoidal.tor
category_theory.monoidal.transport
category_theory.monoidal.types
category_theory.natural_isomorphism
category_theory.natural_transformation
category_theory.opposites
category_theory.over
category_theory.path_category
category_theory.pempty
category_theory.pi.basic
category_theory.preadditive.Mat
category_theory.preadditive.additive_functor
category_theory.preadditive.biproducts
category_theory.preadditive.default
category_theory.preadditive.functor_category
category_theory.preadditive.opposite
category_theory.preadditive.projective
category_theory.preadditive.projective_resolution
category_theory.preadditive.schur
category_theory.preadditive.single_obj
category_theory.products.associator
category_theory.products.basic
category_theory.products.bifunctor
category_theory.punit
category_theory.quotient
category_theory.reflects_isomorphisms
category_theory.shift
category_theory.sigma.basic
category_theory.simple
category_theory.single_obj
category_theory.sites.canonical
category_theory.sites.closed
category_theory.sites.grothendieck
category_theory.sites.pretopology
category_theory.sites.sheaf
category_theory.sites.sheaf_of_types
category_theory.sites.sieves
category_theory.sites.spaces
category_theory.sites.types
category_theory.skeletal
category_theory.structured_arrow
category_theory.subobject.basic
category_theory.subobject.factor_thru
category_theory.subobject.lattice
category_theory.subobject.limits
category_theory.subobject.mono_over
category_theory.subobject.types
category_theory.subobject.well_powered
category_theory.subterminal
category_theory.sums.associator
category_theory.sums.basic
category_theory.thin
category_theory.triangulated.basic
category_theory.triangulated.pretriangulated
category_theory.triangulated.rotate
category_theory.types
category_theory.whiskering
category_theory.with_terminal
category_theory.yoneda
combinatorics.choose.bounds
combinatorics.colex
combinatorics.composition
combinatorics.derangements.basic
combinatorics.derangements.exponential
combinatorics.derangements.finite
combinatorics.hales_jewett
combinatorics.hall
combinatorics.partition
combinatorics.pigeonhole
combinatorics.quiver
combinatorics.simple_graph.adj_matrix
combinatorics.simple_graph.basic
combinatorics.simple_graph.degree_sum
combinatorics.simple_graph.matching
combinatorics.simple_graph.strongly_regular
combinatorics.simple_graph.subgraph
computability.DFA
computability.NFA
computability.encoding
computability.epsilon_NFA
computability.halting
computability.language
computability.partrec
computability.partrec_code
computability.primrec
computability.reduce
computability.regular_expressions
computability.tm_computable
computability.tm_to_partrec
computability.turing_machine
control.applicative
control.basic
control.bifunctor
control.bitraversable.basic
control.bitraversable.instances
control.bitraversable.lemmas
control.equiv_functor
control.equiv_functor.instances
control.fix
control.fold
control.functor
control.functor.multivariate
control.lawful_fix
control.monad.basic
control.monad.cont
control.monad.writer
control.traversable.basic
control.traversable.derive
control.traversable.equiv
control.traversable.instances
control.traversable.lemmas
control.ulift
control.uliftable
data.W
data.analysis.filter
data.analysis.topology
data.array.lemmas
data.bitvec.basic
data.bitvec.core
data.bool
data.bracket
data.buffer.basic
data.buffer.parser.basic
data.buffer.parser.numeral
data.bundle
data.char
data.complex.basic
data.complex.exponential
data.complex.exponential_bounds
data.complex.is_R_or_C
data.complex.module
data.dfinsupp
data.dlist.basic
data.dlist.instances
data.equiv.basic
data.equiv.denumerable
data.equiv.embedding
data.equiv.encodable.basic
data.equiv.encodable.lattice
data.equiv.encodable.small
data.equiv.fin
data.equiv.fintype
data.equiv.functor
data.equiv.list
data.equiv.local_equiv
data.equiv.mul_add
data.equiv.mul_add_aut
data.equiv.nat
data.equiv.option
data.equiv.ring
data.equiv.ring_aut
data.equiv.transfer_instance
data.erased
data.fin
data.fin2
data.fin_enum
data.finmap
data.finset.basic
data.finset.fold
data.finset.intervals
data.finset.lattice
data.finset.nat_antidiagonal
data.finset.noncomm_prod
data.finset.order
data.finset.pi
data.finset.pi_induction
data.finset.pimage
data.finset.powerset
data.finset.preimage
data.finset.sort
data.finsupp.antidiagonal
data.finsupp.basic
data.finsupp.default
data.finsupp.lattice
data.finsupp.pointwise
data.finsupp.to_dfinsupp
data.fintype.basic
data.fintype.card
data.fintype.card_embedding
data.fintype.fin
data.fintype.intervals
data.fintype.list
data.fintype.small
data.fintype.sort
data.fp.basic
data.hash_map
data.holor
data.int.absolute_value
data.int.basic
data.int.cast
data.int.char_zero
data.int.gcd
data.int.least_greatest
data.int.modeq
data.int.nat_prime
data.int.order
data.int.parity
data.int.range
data.int.sqrt
data.lazy_list
data.lazy_list.basic
data.list.alist
data.list.bag_inter
data.list.basic
data.list.chain
data.list.cycle
data.list.defs
data.list.duplicate
data.list.erase_dup
data.list.forall2
data.list.func
data.list.indexes
data.list.intervals
data.list.min_max
data.list.nat_antidiagonal
data.list.nodup
data.list.nodup_equiv_fin
data.list.of_fn
data.list.pairwise
data.list.palindrome
data.list.perm
data.list.range
data.list.rotate
data.list.sections
data.list.sigma
data.list.sort
data.list.sublists
data.list.tfae
data.list.zip
data.matrix.basic
data.matrix.basis
data.matrix.block
data.matrix.char_p
data.matrix.dmatrix
data.matrix.hadamard
data.matrix.kronecker
data.matrix.notation
data.matrix.pequiv
data.mllist
data.multiset.antidiagonal
data.multiset.basic
data.multiset.erase_dup
data.multiset.finset_ops
data.multiset.fold
data.multiset.functor
data.multiset.intervals
data.multiset.lattice
data.multiset.nat_antidiagonal
data.multiset.nodup
data.multiset.pi
data.multiset.powerset
data.multiset.range
data.multiset.sections
data.multiset.sort
data.mv_polynomial.basic
data.mv_polynomial.comap
data.mv_polynomial.comm_ring
data.mv_polynomial.counit
data.mv_polynomial.equiv
data.mv_polynomial.expand
data.mv_polynomial.funext
data.mv_polynomial.invertible
data.mv_polynomial.monad
data.mv_polynomial.pderiv
data.mv_polynomial.rename
data.mv_polynomial.variables
data.nat.basic
data.nat.bitwise
data.nat.cast
data.nat.choose.basic
data.nat.choose.dvd
data.nat.choose.sum
data.nat.choose.vandermonde
data.nat.digits
data.nat.dist
data.nat.enat
data.nat.factorial
data.nat.fib
data.nat.gcd
data.nat.lattice
data.nat.log
data.nat.modeq
data.nat.mul_ind
data.nat.multiplicity
data.nat.pairing
data.nat.parity
data.nat.pow
data.nat.prime
data.nat.psub
data.nat.sqrt
data.nat.totient
data.nat.upto
data.nat.with_bot
data.num.basic
data.num.bitwise
data.num.lemmas
data.num.prime
data.opposite
data.option.basic
data.option.defs
data.ordmap.ordnode
data.ordmap.ordset
data.part
data.pequiv
data.pfun
data.pfunctor.multivariate.M
data.pfunctor.multivariate.W
data.pfunctor.multivariate.basic
data.pfunctor.univariate.M
data.pfunctor.univariate.basic
data.pi
data.pnat.basic
data.pnat.factors
data.pnat.intervals
data.pnat.prime
data.pnat.xgcd
data.polynomial.algebra_map
data.polynomial.basic
data.polynomial.cancel_leads
data.polynomial.coeff
data.polynomial.degree.card_pow_degree
data.polynomial.degree.definitions
data.polynomial.degree.lemmas
data.polynomial.degree.trailing_degree
data.polynomial.denoms_clearable
data.polynomial.derivative
data.polynomial.div
data.polynomial.erase_lead
data.polynomial.eval
data.polynomial.field_division
data.polynomial.hasse_deriv
data.polynomial.identities
data.polynomial.induction
data.polynomial.inductions
data.polynomial.integral_normalization
data.polynomial.iterated_deriv
data.polynomial.lifts
data.polynomial.mirror
data.polynomial.monic
data.polynomial.monomial
data.polynomial.reverse
data.polynomial.ring_division
data.polynomial.taylor
data.pprod
data.prod
data.qpf.multivariate.basic
data.qpf.multivariate.constructions.cofix
data.qpf.multivariate.constructions.comp
data.qpf.multivariate.constructions.const
data.qpf.multivariate.constructions.fix
data.qpf.multivariate.constructions.prj
data.qpf.multivariate.constructions.quot
data.qpf.multivariate.constructions.sigma
data.qpf.univariate.basic
data.quot
data.rat.basic
data.rat.cast
data.rat.default
data.rat.denumerable
data.rat.floor
data.rat.meta_defs
data.rat.order
data.rat.sqrt
data.real.basic
data.real.cardinality
data.real.cau_seq
data.real.cau_seq_completion
data.real.conjugate_exponents
data.real.ennreal
data.real.ereal
data.real.golden_ratio
data.real.hyperreal
data.real.irrational
data.real.nnreal
data.real.pi
data.real.sign
data.real.sqrt
data.rel
data.semiquot
data.seq.computation
data.seq.parallel
data.seq.seq
data.seq.wseq
data.set.Union_lift
data.set.accumulate
data.set.basic
data.set.bool
data.set.constructions
data.set.countable
data.set.enumerate
data.set.finite
data.set.function
data.set.intervals.basic
data.set.intervals.disjoint
data.set.intervals.image_preimage
data.set.intervals.infinite
data.set.intervals.ord_connected
data.set.intervals.pi
data.set.intervals.proj_Icc
data.set.intervals.surj_on
data.set.intervals.unordered_interval
data.set.lattice
data.set.pairwise
data.set_like.basic
data.set_like.fintype
data.setoid.basic
data.setoid.partition
data.sigma.basic
data.stream.basic
data.string.basic
data.string.defs
data.subtype
data.sum
data.sym.basic
data.sym.card
data.sym.sym2
data.tprod
data.tree
data.typevec
data.ulift
data.vector.basic
data.vector3
data.zmod.algebra
data.zmod.basic
data.zmod.parity
data.zmod.quotient
deprecated.group
deprecated.ring
deprecated.subfield
deprecated.subgroup
deprecated.submonoid
deprecated.subring
dynamics.circle.rotation_number.translation_number
dynamics.ergodic.conservative
dynamics.ergodic.measure_preserving
dynamics.fixed_points.basic
dynamics.fixed_points.topology
dynamics.flow
dynamics.omega_limit
dynamics.periodic_pts
field_theory.abel_ruffini
field_theory.adjoin
field_theory.algebraic_closure
field_theory.chevalley_warning
field_theory.finite.basic
field_theory.finite.galois_field
field_theory.finite.polynomial
field_theory.finiteness
field_theory.fixed
field_theory.galois
field_theory.intermediate_field
field_theory.minpoly
field_theory.mv_polynomial
field_theory.normal
field_theory.perfect_closure
field_theory.polynomial_galois_group
field_theory.primitive_element
field_theory.separable
field_theory.separable_degree
field_theory.splitting_field
field_theory.subfield
field_theory.tower
geometry.euclidean.basic
geometry.euclidean.circumcenter
geometry.euclidean.monge_point
geometry.euclidean.sphere
geometry.euclidean.triangle
geometry.manifold.algebra.left_invariant_derivation
geometry.manifold.algebra.lie_group
geometry.manifold.algebra.monoid
geometry.manifold.algebra.smooth_functions
geometry.manifold.algebra.structures
geometry.manifold.basic_smooth_bundle
geometry.manifold.bump_function
geometry.manifold.charted_space
geometry.manifold.conformal_groupoid
geometry.manifold.derivation_bundle
geometry.manifold.diffeomorph
geometry.manifold.instances.real
geometry.manifold.instances.sphere
geometry.manifold.instances.units_of_normed_algebra
geometry.manifold.local_invariant_properties
geometry.manifold.mfderiv
geometry.manifold.partition_of_unity
geometry.manifold.smooth_manifold_with_corners
geometry.manifold.times_cont_mdiff
geometry.manifold.times_cont_mdiff_map
geometry.manifold.whitney_embedding
group_theory.abelianization
group_theory.archimedean
group_theory.complement
group_theory.congruence
group_theory.coset
group_theory.eckmann_hilton
group_theory.finiteness
group_theory.free_abelian_group
group_theory.free_abelian_group_finsupp
group_theory.free_group
group_theory.free_product
group_theory.general_commutator
group_theory.group_action.basic
group_theory.group_action.defs
group_theory.group_action.group
group_theory.group_action.prod
group_theory.group_action.sub_mul_action
group_theory.group_action.units
group_theory.index
group_theory.is_free_group
group_theory.monoid_localization
group_theory.nielsen_schreier
group_theory.nilpotent
group_theory.order_of_element
group_theory.p_group
group_theory.perm.basic
group_theory.perm.concrete_cycle
group_theory.perm.cycle_type
group_theory.perm.cycles
group_theory.perm.fin
group_theory.perm.list
group_theory.perm.option
group_theory.perm.sign
group_theory.perm.subgroup
group_theory.perm.support
group_theory.presented_group
group_theory.quotient_group
group_theory.semidirect_product
group_theory.solvable
group_theory.specific_groups.alternating
group_theory.specific_groups.cyclic
group_theory.specific_groups.dihedral
group_theory.specific_groups.quaternion
group_theory.subgroup
group_theory.submonoid.basic
group_theory.submonoid.center
group_theory.submonoid.membership
group_theory.submonoid.operations
group_theory.sylow
linear_algebra.adic_completion
linear_algebra.affine_space.affine_equiv
linear_algebra.affine_space.affine_map
linear_algebra.affine_space.affine_subspace
linear_algebra.affine_space.basic
linear_algebra.affine_space.combination
linear_algebra.affine_space.finite_dimensional
linear_algebra.affine_space.independent
linear_algebra.affine_space.midpoint
linear_algebra.affine_space.ordered
linear_algebra.alternating
linear_algebra.basic
linear_algebra.basis
linear_algebra.bilinear_form
linear_algebra.bilinear_map
linear_algebra.char_poly.basic
linear_algebra.char_poly.coeff
linear_algebra.clifford_algebra.basic
linear_algebra.clifford_algebra.conjugation
linear_algebra.clifford_algebra.equivs
linear_algebra.coevaluation
linear_algebra.contraction
linear_algebra.determinant
linear_algebra.dfinsupp
linear_algebra.dimension
linear_algebra.direct_sum.finsupp
linear_algebra.direct_sum.tensor_product
linear_algebra.dual
linear_algebra.eigenspace
linear_algebra.exterior_algebra
linear_algebra.finite_dimensional
linear_algebra.finsupp
linear_algebra.finsupp_vector_space
linear_algebra.free_algebra
linear_algebra.free_module
linear_algebra.free_module_pid
linear_algebra.invariant_basis_number
linear_algebra.lagrange
linear_algebra.linear_independent
linear_algebra.linear_pmap
linear_algebra.matrix.absolute_value
linear_algebra.matrix.basis
linear_algebra.matrix.block
linear_algebra.matrix.circulant
linear_algebra.matrix.determinant
linear_algebra.matrix.diagonal
linear_algebra.matrix.dot_product
linear_algebra.matrix.dual
linear_algebra.matrix.finite_dimensional
linear_algebra.matrix.is_diag
linear_algebra.matrix.nonsingular_inverse
linear_algebra.matrix.orthogonal
linear_algebra.matrix.polynomial
linear_algebra.matrix.reindex
linear_algebra.matrix.symmetric
linear_algebra.matrix.to_lin
linear_algebra.matrix.to_linear_equiv
linear_algebra.matrix.trace
linear_algebra.matrix.transvection
linear_algebra.multilinear
linear_algebra.pi
linear_algebra.pi_tensor_product
linear_algebra.prod
linear_algebra.projection
linear_algebra.quadratic_form
linear_algebra.sesquilinear_form
linear_algebra.smodeq
linear_algebra.special_linear_group
linear_algebra.std_basis
linear_algebra.tensor_algebra
linear_algebra.tensor_product
linear_algebra.tensor_product_basis
linear_algebra.trace
linear_algebra.unitary_group
linear_algebra.vandermonde
logic.basic
logic.embedding
logic.function.basic
logic.function.conjugate
logic.function.iterate
logic.is_empty
logic.nontrivial
logic.relation
logic.relator
logic.small
logic.unique
measure_theory.category.Meas
measure_theory.constructions.borel_space
measure_theory.constructions.pi
measure_theory.constructions.prod
measure_theory.decomposition.jordan
measure_theory.decomposition.lebesgue
measure_theory.decomposition.radon_nikodym
measure_theory.decomposition.signed_hahn
measure_theory.decomposition.unsigned_hahn
measure_theory.function.ae_eq_fun
measure_theory.function.ae_eq_of_integral
measure_theory.function.ae_measurable_sequence
measure_theory.function.conditional_expectation
measure_theory.function.continuous_map_dense
measure_theory.function.ess_sup
measure_theory.function.l1_space
measure_theory.function.l2_space
measure_theory.function.lp_space
measure_theory.function.simple_func_dense
measure_theory.function.special_functions
measure_theory.function.strongly_measurable
measure_theory.group.arithmetic
measure_theory.group.basic
measure_theory.group.prod
measure_theory.integral.bochner
measure_theory.integral.integrable_on
measure_theory.integral.integral_eq_improper
measure_theory.integral.interval_integral
measure_theory.integral.lebesgue
measure_theory.integral.mean_inequalities
measure_theory.integral.set_integral
measure_theory.integral.set_to_l1
measure_theory.integral.vitali_caratheodory
measure_theory.measurable_space
measure_theory.measurable_space_def
measure_theory.measure.content
measure_theory.measure.giry_monad
measure_theory.measure.haar
measure_theory.measure.haar_lebesgue
measure_theory.measure.hausdorff
measure_theory.measure.lebesgue
measure_theory.measure.measure_space
measure_theory.measure.measure_space_def
measure_theory.measure.outer_measure
measure_theory.measure.regular
measure_theory.measure.stieltjes
measure_theory.measure.vector_measure
measure_theory.measure.with_density_vector_measure
measure_theory.pi_system
measure_theory.probability_mass_function
measure_theory.tactic
meta.coinductive_predicates
meta.expr
meta.expr_lens
meta.rb_map
meta.uchange
model_theory.basic
number_theory.ADE_inequality
number_theory.arithmetic_function
number_theory.basic
number_theory.bernoulli
number_theory.bernoulli_polynomials
number_theory.class_number.admissible_abs
number_theory.class_number.admissible_absolute_value
number_theory.class_number.admissible_card_pow_degree
number_theory.dioph
number_theory.divisors
number_theory.fermat4
number_theory.function_field
number_theory.l_series
number_theory.liouville.basic
number_theory.liouville.liouville_constant
number_theory.lucas_lehmer
number_theory.number_field
number_theory.padics.hensel
number_theory.padics.padic_integers
number_theory.padics.padic_norm
number_theory.padics.padic_numbers
number_theory.padics.ring_homs
number_theory.pell
number_theory.primes_congruent_one
number_theory.primorial
number_theory.pythagorean_triples
number_theory.quadratic_reciprocity
number_theory.sum_four_squares
number_theory.sum_two_squares
number_theory.zsqrtd.basic
number_theory.zsqrtd.gaussian_int
number_theory.zsqrtd.to_real
order.atoms
order.basic
order.boolean_algebra
order.bounded_lattice
order.bounds
order.category.LinearOrder
order.category.NonemptyFinLinOrd
order.category.PartialOrder
order.category.Preorder
order.category.omega_complete_partial_order
order.closure
order.compactly_generated
order.complete_boolean_algebra
order.complete_lattice
order.conditionally_complete_lattice
order.copy
order.countable_dense_linear_order
order.directed
order.disjointed
order.extension
order.filter.archimedean
order.filter.at_top_bot
order.filter.bases
order.filter.basic
order.filter.cofinite
order.filter.countable_Inter
order.filter.ennreal
order.filter.extr
order.filter.filter_product
order.filter.germ
order.filter.indicator_function
order.filter.interval
order.filter.lift
order.filter.partial
order.filter.pointwise
order.filter.ultrafilter
order.fixed_points
order.galois_connection
order.ideal
order.iterate
order.lattice
order.lattice_intervals
order.lexicographic
order.liminf_limsup
order.modular_lattice
order.omega_complete_partial_order
order.ord_continuous
order.order_dual
order.order_iso_nat
order.partial_sups
order.pfilter
order.pilex
order.preorder_hom
order.prime_ideal
order.rel_classes
order.rel_iso
order.semiconj_Sup
order.symm_diff
order.well_founded
order.well_founded_set
order.zorn
probability_theory.independence
probability_theory.integration
representation_theory.maschke
ring_theory.adjoin.basic
ring_theory.adjoin.power_basis
ring_theory.adjoin_root
ring_theory.algebra_tower
ring_theory.algebraic
ring_theory.artinian
ring_theory.class_group
ring_theory.coprime
ring_theory.dedekind_domain
ring_theory.derivation
ring_theory.discrete_valuation_ring
ring_theory.eisenstein_criterion
ring_theory.euclidean_domain
ring_theory.finiteness
ring_theory.fintype
ring_theory.flat
ring_theory.fractional_ideal
ring_theory.free_comm_ring
ring_theory.free_ring
ring_theory.hahn_series
ring_theory.ideal.basic
ring_theory.ideal.local_ring
ring_theory.ideal.operations
ring_theory.ideal.over
ring_theory.ideal.prod
ring_theory.int.basic
ring_theory.integral_closure
ring_theory.integral_domain
ring_theory.integrally_closed
ring_theory.jacobson
ring_theory.jacobson_ideal
ring_theory.laurent_series
ring_theory.localization
ring_theory.matrix_algebra
ring_theory.multiplicity
ring_theory.mv_polynomial.basic
ring_theory.nakayama
ring_theory.nilpotent
ring_theory.noetherian
ring_theory.non_zero_divisors
ring_theory.norm
ring_theory.nullstellensatz
ring_theory.perfection
ring_theory.polynomial.basic
ring_theory.polynomial.bernstein
ring_theory.polynomial.chebyshev
ring_theory.polynomial.content
ring_theory.polynomial.cyclotomic
ring_theory.polynomial.dickson
ring_theory.polynomial.gauss_lemma
ring_theory.polynomial.homogeneous
ring_theory.polynomial.pochhammer
ring_theory.polynomial.rational_root
ring_theory.polynomial.scale_roots
ring_theory.polynomial.symmetric
ring_theory.polynomial.tower
ring_theory.polynomial.vieta
ring_theory.polynomial_algebra
ring_theory.power_basis
ring_theory.power_series.basic
ring_theory.power_series.well_known
ring_theory.prime
ring_theory.principal_ideal_domain
ring_theory.ring_invo
ring_theory.roots_of_unity
ring_theory.simple_module
ring_theory.subring
ring_theory.subsemiring
ring_theory.tensor_product
ring_theory.trace
ring_theory.unique_factorization_domain
ring_theory.valuation.basic
ring_theory.valuation.integers
ring_theory.valuation.integral
ring_theory.witt_vector.basic
ring_theory.witt_vector.compare
ring_theory.witt_vector.defs
ring_theory.witt_vector.frobenius
ring_theory.witt_vector.identities
ring_theory.witt_vector.init_tail
ring_theory.witt_vector.is_poly
ring_theory.witt_vector.mul_p
ring_theory.witt_vector.structure_polynomial
ring_theory.witt_vector.teichmuller
ring_theory.witt_vector.truncated
ring_theory.witt_vector.verschiebung
ring_theory.witt_vector.witt_polynomial
set_theory.cardinal
set_theory.cardinal_ordinal
set_theory.cofinality
set_theory.fincard
set_theory.game
set_theory.game.domineering
set_theory.game.impartial
set_theory.game.nim
set_theory.game.short
set_theory.game.state
set_theory.game.winner
set_theory.lists
set_theory.ordinal
set_theory.ordinal_arithmetic
set_theory.ordinal_notation
set_theory.pgame
set_theory.schroeder_bernstein
set_theory.surreal.basic
set_theory.surreal.dyadic
set_theory.zfc
system.random.basic
tactic.abel
tactic.algebra
tactic.alias
tactic.apply
tactic.apply_fun
tactic.auto_cases
tactic.binder_matching
tactic.cache
tactic.cancel_denoms
tactic.chain
tactic.choose
tactic.clear
tactic.congr
tactic.converter.apply_congr
tactic.converter.binders
tactic.converter.interactive
tactic.converter.old_conv
tactic.core
tactic.dec_trivial
tactic.delta_instance
tactic.dependencies
tactic.derive_fintype
tactic.derive_inhabited
tactic.doc_commands
tactic.elementwise
tactic.elide
tactic.equiv_rw
tactic.explode
tactic.explode_widget
tactic.ext
tactic.field_simp
tactic.fin_cases
tactic.find
tactic.find_unused
tactic.finish
tactic.fix_reflect_string
tactic.fresh_names
tactic.generalize_proofs
tactic.generalizes
tactic.group
tactic.has_variable_names
tactic.hint
tactic.induction
tactic.interactive
tactic.interactive_expr
tactic.interval_cases
tactic.itauto
tactic.lean_core_docs
tactic.lift
tactic.linarith.datatypes
tactic.linarith.elimination
tactic.linarith.frontend
tactic.linarith.lemmas
tactic.linarith.parsing
tactic.linarith.preprocessing
tactic.linarith.verification
tactic.lint.basic
tactic.lint.default
tactic.lint.frontend
tactic.lint.misc
tactic.lint.simp
tactic.lint.type_classes
tactic.local_cache
tactic.localized
tactic.mk_iff_of_inductive_prop
tactic.monotonicity.basic
tactic.monotonicity.interactive
tactic.monotonicity.lemmas
tactic.noncomm_ring
tactic.norm_cast
tactic.norm_fin
tactic.norm_num
tactic.norm_swap
tactic.nth_rewrite.basic
tactic.nth_rewrite.congr
tactic.nth_rewrite.default
tactic.obviously
tactic.omega.clause
tactic.omega.coeffs
tactic.omega.eq_elim
tactic.omega.find_ees
tactic.omega.find_scalars
tactic.omega.int.dnf
tactic.omega.int.form
tactic.omega.int.main
tactic.omega.int.preterm
tactic.omega.lin_comb
tactic.omega.main
tactic.omega.misc
tactic.omega.nat.dnf
tactic.omega.nat.form
tactic.omega.nat.main
tactic.omega.nat.neg_elim
tactic.omega.nat.preterm
tactic.omega.nat.sub_elim
tactic.omega.prove_unsats
tactic.omega.term
tactic.pi_instances
tactic.pretty_cases
tactic.protected
tactic.push_neg
tactic.rcases
tactic.reassoc_axiom
tactic.rename_var
tactic.replacer
tactic.reserved_notation
tactic.restate_axiom
tactic.rewrite
tactic.rewrite_all.basic
tactic.rewrite_search.discovery
tactic.rewrite_search.explain
tactic.rewrite_search.frontend
tactic.rewrite_search.search
tactic.rewrite_search.types
tactic.ring
tactic.ring2
tactic.ring_exp
tactic.scc
tactic.show_term
tactic.simp_command
tactic.simp_result
tactic.simp_rw
tactic.simpa
tactic.simps
tactic.slice
tactic.slim_check
tactic.solve_by_elim
tactic.split_ifs
tactic.squeeze
tactic.subtype_instance
tactic.suggest
tactic.tauto
tactic.tfae
tactic.tidy
tactic.transform_decl
tactic.transport
tactic.trunc_cases
tactic.unfold_cases
tactic.unify_equations
tactic.where
tactic.with_local_reducibility
tactic.wlog
tactic.zify
testing.slim_check.functions
testing.slim_check.gen
testing.slim_check.sampleable
testing.slim_check.testable
topology.G_delta
topology.alexandroff
topology.algebra.affine
topology.algebra.algebra
topology.algebra.field
topology.algebra.floor_ring
topology.algebra.group
topology.algebra.group_completion
topology.algebra.group_with_zero
topology.algebra.infinite_sum
topology.algebra.localization
topology.algebra.module
topology.algebra.monoid
topology.algebra.mul_action
topology.algebra.multilinear
topology.algebra.nonarchimedean.basic
topology.algebra.open_subgroup
topology.algebra.ordered.basic
topology.algebra.ordered.extend_from
topology.algebra.ordered.liminf_limsup
topology.algebra.ordered.proj_Icc
topology.algebra.polynomial
topology.algebra.ring
topology.algebra.uniform_field
topology.algebra.uniform_group
topology.algebra.uniform_ring
topology.algebra.weak_dual_topology
topology.bases
topology.basic
topology.category.CompHaus.default
topology.category.CompHaus.projective
topology.category.Compactum
topology.category.Profinite.as_limit
topology.category.Profinite.cofiltered_limit
topology.category.Profinite.default
topology.category.Profinite.projective
topology.category.Top.adjunctions
topology.category.Top.basic
topology.category.Top.epi_mono
topology.category.Top.limits
topology.category.Top.open_nhds
topology.category.Top.opens
topology.category.TopCommRing
topology.category.UniformSpace
topology.compact_open
topology.compacts
topology.connected
topology.constructions
topology.continuous_function.algebra
topology.continuous_function.basic
topology.continuous_function.bounded
topology.continuous_function.compact
topology.continuous_function.polynomial
topology.continuous_function.stone_weierstrass
topology.continuous_function.weierstrass
topology.continuous_on
topology.dense_embedding
topology.discrete_quotient
topology.extend_from
topology.fiber_bundle
topology.homeomorph
topology.homotopy
topology.instances.ennreal
topology.instances.ereal
topology.instances.nnreal
topology.instances.real
topology.instances.real_vector_space
topology.list
topology.local_extr
topology.local_homeomorph
topology.locally_constant.algebra
topology.locally_constant.basic
topology.maps
topology.metric_space.algebra
topology.metric_space.antilipschitz
topology.metric_space.baire
topology.metric_space.basic
topology.metric_space.cau_seq_filter
topology.metric_space.closeds
topology.metric_space.completion
topology.metric_space.contracting
topology.metric_space.emetric_paracompact
topology.metric_space.emetric_space
topology.metric_space.gluing
topology.metric_space.gromov_hausdorff
topology.metric_space.gromov_hausdorff_realized
topology.metric_space.hausdorff_distance
topology.metric_space.holder
topology.metric_space.isometry
topology.metric_space.kuratowski
topology.metric_space.lipschitz
topology.metric_space.metric_separated
topology.metric_space.shrinking_lemma
topology.omega_complete_partial_order
topology.opens
topology.order
topology.paracompact
topology.partition_of_unity
topology.path_connected
topology.semicontinuous
topology.separation
topology.sequences
topology.sheaves.forget
topology.sheaves.limits
topology.sheaves.local_predicate
topology.sheaves.presheaf
topology.sheaves.presheaf_of_functions
topology.sheaves.sheaf
topology.sheaves.sheaf_condition.equalizer_products
topology.sheaves.sheaf_condition.opens_le_cover
topology.sheaves.sheaf_condition.pairwise_intersections
topology.sheaves.sheaf_condition.unique_gluing
topology.sheaves.sheaf_of_functions
topology.sheaves.sheafify
topology.sheaves.stalks
topology.shrinking_lemma
topology.stone_cech
topology.subset_properties
topology.tactic
topology.uniform_space.absolute_value
topology.uniform_space.abstract_completion
topology.uniform_space.basic
topology.uniform_space.cauchy
topology.uniform_space.compact_separated
topology.uniform_space.compare_reals
topology.uniform_space.complete_separated
topology.uniform_space.completion
topology.uniform_space.pi
topology.uniform_space.separation
topology.uniform_space.uniform_convergence
topology.uniform_space.uniform_embedding
topology.unit_interval
topology.urysohns_lemma
topology.vector_bundle

debugger.attr

source

meta def debugger.attr :

(user_attribute unit)

General documentation

Additional documentation

mathlib overview

tactic writing

calc mode

conv mode

simplification

well founded recursion

style guide

documentation style guide

naming conventions

Library

core

data

buffer

parser

buffer

dlist

stream

vector

init

algebra

classes

functions

order

control

alternative

applicative

combinators

except

functor

id

lawful

lift

monad

monad_fail

option

reader

state

data

array

basic

slice

bool

basic

lemmas

char

basic

classes

lemmas

fin

basic

ops

int

basic

bitwise

comp_lemmas

order

list

basic

instances

lemmas

qsort

nat

basic

bitwise

div

gcd

lemmas

option

basic

instances

ordering

basic

lemmas

rbmap

basic

rbtree

basic

default

sigma

basic

lex

string

basic

ops

subtype

basic

instances

sum

basic

unsigned

basic

ops

prod

punit

quot

repr

set

setoid

to_string

mathlib

algebra

basic

operations

ordered

restrict_scalars

subalgebra

tower

big_operators

basic

enat

fin

finprod

finsupp

intervals

nat_antidiagonal

order

pi

ring

category

Algebra

basic

limits

CommRing

adjunctions

basic

colimits

limits

Group

Z_Module_equivalence

abelian

adjunctions

basic

biproducts

colimits

images

limits

preadditive

subobject

zero

Module

abelian

adjunctions

basic

colimits

epi_mono

kernels

limits

monoidal

projective

subobject

Mon

adjunctions

basic

colimits

limits

Semigroup

basic

FinVect

char_p

algebra

basic

exp_char

invertible

pi

quotient

subring

continued_fractions

computation

approximation_corollaries

approximations

basic

correctness_terminating

default

terminates_iff_rat

translations

basic

continuants_recurrence

convergents_equiv

default

terminated_stable

translations

direct_sum

algebra

basic

finsupp

module

ring

gcd_monoid

basic

finset

multiset

group

basic

commute

conj

default

defs

hom

hom_instances

inj_surj

pi

prod

semiconj

to_additive

type_tags

ulift

units

units_hom

with_one

group_power

basic

identities

lemmas

order

group_with_zero

basic

defs

power

homology

additive

augment

complex_shape

differential_object

exact

flip

functor

homological_complex

homology

homotopy

homotopy_category

image_to_kernel

quasi_iso

single

lie

abelian

base_change

basic

cartan_matrix

cartan_subalgebra

character

classical

direct_sum

free

ideal_operations

matrix

nilpotent

non_unital_non_assoc_algebra

of_associative

quotient

semisimple

skew_adjoint

solvable

subalgebra

submodule

tensor_product

universal_enveloping

weights

module

basic

default

hom

linear_map

opposites

ordered

pi

prod

projective

submodule

submodule_lattice

ulift

monoid_algebra

basic

to_direct_sum

polynomial

big_operators

group_ring_action

regular

basic

pow

smul

ring

basic

boolean_ring

default

pi

prod

ulift

star

algebra

basic

chsh

pi

tropical

basic

absolute_value

add_torsor

archimedean

associated

bounds

char_zero

covariant_and_contravariant

direct_limit

divisibility

euclidean_absolute_value

euclidean_domain

field

field_power

floor

free

free_algebra

free_monoid

free_non_unital_non_assoc_algebra

geom_sum

group_action_hom

group_ring_action

hierarchy_design

indicator_function

invertible

iterate_hom

lattice_ordered_group

linear_ordered_comm_group_with_zero

linear_recurrence

non_unital_alg_hom

opposites

order

order_functions

ordered_field

ordered_group

ordered_monoid

ordered_monoid_lemmas

ordered_pi

ordered_pointwise

ordered_ring

ordered_smul

ordered_sub

pempty_instances

periodic

pointwise

punit_instances

quadratic_discriminant

quandle

quaternion

quaternion_basis

ring_quot

smul_with_zero

squarefree

support

triv_sq_zero_ext

algebraic_geometry

presheafed_space

has_colimits

EllipticCurve

Scheme

Spec

is_open_comap_C

locally_ringed_space

presheafed_space

prime_spectrum

sheafed_space

stalks

structure_sheaf

algebraic_topology

Moore_complex

cech_nerve

simplex_category

simplicial_object

simplicial_set

topological_simplex

analysis

ODE

gronwall

analytic

basic

composition

inverse

linear

radius_liminf

asymptotics

asymptotic_equivalent

asymptotics

specific_asymptotics

calculus

conformal

darboux

deriv

extend_deriv

fderiv

fderiv_measurable

fderiv_symmetric

formal_multilinear_series

implicit

inverse

iterated_deriv

lagrange_multipliers

lhopital

local_extr

mean_value

parametric_integral

specific_functions

tangent_cone

times_cont_diff

complex

basic

circle

conformal

isometry

polynomial

real_deriv

roots_of_unity

upper_half_plane

convex

basic

caratheodory

combination

cone

exposed

extrema

extreme

independent

integral

specific_functions

topology

normed_space

SemiNormedGroup

kernels

SemiNormedGroup

add_torsor

affine_isometry

banach

basic

bounded_linear_maps

complemented

conformal_linear_map

dual

enorm

euclidean_dist

exponential

extend

finite_dimension

hahn_banach

indicator_function

inner_product

int

linear_isometry

mazur_ulam

multilinear

normed_group_hom

normed_group_hom_completion

normed_group_quotient

operator_norm

ordered

pi_Lp

riesz_lemma

units

weak_dual

special_functions

arsinh

bernstein

exp_log

integrals

polynomials

pow

sqrt

trigonometric

fourier

hofer

mean_inequalities

p_series

quaternion

seminorm

specific_limits

category_theory

abelian

diagram_lemmas

four

basic

exact

ext

non_preadditive

opposite

projective

pseudoelements

additive

basic

adjunction

adjoint_functor_theorems

basic

comma

fully_faithful

lifting

limits

mates

opposites

over

reflective

category

Cat

Groupoid

Kleisli

Quiv

Rel

default

pairwise

preorder

ulift

closed

cartesian

functor

ideal

monoidal

types

zero

concrete_category

basic

bundled

bundled_hom

reflects_isomorphisms

unbundled_hom

enriched

basic

limits

constructions

over

connected

default

products

binary_products

epi_mono

equalizers

finite_products_of_binary_products

limits_of_products_and_equalizers

pullbacks

weakly_initial

preserves

shapes

binary_products

equalizers

products

pullbacks

terminal

basic

functor_category

limits

shapes

binary_products

biproducts

concrete_category

disjoint_coproduct

equalizers

finite_limits

finite_products

images

kernel_pair

kernels

normal_mono

products

pullbacks

reflexive

regular_mono

split_coequalizer

strict_initial

strong_epi

terminal

types

wide_equalizers

wide_pullbacks

zero

colimit_limit

comma

concrete_category

cones

connected

creates

filtered_colimit_commutes_finite_limit

final

fubini

functor_category

has_limits

is_limit

kan_extension

lattice

opposites

over

pi

presheaf

punit

small_complete

types

yoneda

linear

default

linear_functor

yoneda

monad

adjunction

algebra

basic

coequalizer

equiv_mon

kleisli

limits

monadicity

products

types

monoidal

free

basic

coherence

internal

Module

functor_category

limits

types

CommMon_

End

Mod

Mon_

braided

category

center

discrete

functor

functor_category

functorial

limits

natural_transformation

of_chosen_finite_products

of_has_finite_products

opposite

preadditive

rigid

skeleton

tor

transport

types

pi

basic

preadditive

Mat

additive_functor

biproducts

default

functor_category

opposite

projective

projective_resolution

schur

single_obj

products

associator

basic

bifunctor

sigma

basic

sites

canonical

closed

grothendieck

pretopology

sheaf

sheaf_of_types

sieves

spaces

types

subobject

basic

factor_thru

lattice

limits

mono_over

types

well_powered

sums

associator

basic

triangulated

basic

pretriangulated

rotate

Fintype

action

arrow

comma

conj

connected_components

const

core

currying

derived

differential_object

discrete_category

elements

endomorphism

epi_mono

eq_to_hom

equivalence

essential_image

essentially_small

filtered

fin_category

full_subcategory

fully_faithful

functor

functor_category

functorial

graded_object

grothendieck

groupoid

hom_functor

is_connected

isomorphism

isomorphism_classes

lifting_properties

natural_isomorphism

natural_transformation

opposites

over

path_category

pempty

punit

quotient

reflects_isomorphisms

shift

simple

single_obj

skeletal

structured_arrow

subterminal

thin

types

whiskering

with_terminal

yoneda

combinatorics

choose

bounds

derangements

basic

exponential

finite

simple_graph

adj_matrix

basic

degree_sum

matching

strongly_regular

subgraph

colex

composition

hales_jewett

hall

partition

pigeonhole

quiver

computability

DFA

NFA

encoding

epsilon_NFA

halting

language

partrec

partrec_code

primrec

reduce

regular_expressions

tm_computable

tm_to_partrec

turing_machine

control

bitraversable

basic

instances

lemmas

equiv_functor

instances

functor

multivariate

monad

basic

cont

writer

traversable

basic

derive

equiv

instances

lemmas

applicative

basic

bifunctor

equiv_functor

fix

fold

functor

lawful_fix

ulift

uliftable

data

analysis

filter

topology

array

lemmas

bitvec

basic

core

buffer

parser

basic

numeral

basic

complex

basic

exponential

exponential_bounds

is_R_or_C

module

dlist

basic

instances

equiv

encodable

basic

lattice

small

basic

denumerable

embedding

fin

fintype

functor

list

local_equiv

mul_add

mul_add_aut

nat

option

ring

ring_aut

transfer_instance

finset

basic

fold

intervals

lattice

nat_antidiagonal

noncomm_prod

order

pi

pi_induction

pimage

powerset

preimage

sort

finsupp

antidiagonal

basic

default

lattice

pointwise

to_dfinsupp

fintype

basic

card

card_embedding

fin

intervals

list

small

sort

fp

basic

int

absolute_value

basic

cast

char_zero

gcd

least_greatest

modeq

nat_prime

order

parity

range

sqrt

lazy_list

basic

list

alist

bag_inter

basic

chain

cycle

defs

duplicate

erase_dup

forall2

func

indexes

intervals

min_max

nat_antidiagonal

nodup

nodup_equiv_fin

of_fn

pairwise

palindrome

perm

range

rotate

sections

sigma

sort

sublists

tfae

zip

matrix

basic

basis

block

char_p

dmatrix

hadamard

kronecker

notation

pequiv

multiset

antidiagonal

basic

erase_dup

finset_ops

fold

functor

intervals

lattice

nat_antidiagonal

nodup

pi

powerset

range

sections

sort

mv_polynomial

basic

comap

comm_ring

counit

equiv

expand

funext

invertible

monad

pderiv

rename

variables

nat

choose

basic

dvd

sum

vandermonde

basic

bitwise

cast

digits

dist

enat

factorial

fib

gcd

lattice

log

modeq

mul_ind

multiplicity

pairing

parity

pow

prime

psub

sqrt

totient

upto

with_bot

num

basic

bitwise

lemmas

prime

option

basic

defs

ordmap

ordnode

ordset

pfunctor

multivariate

M

W

basic

univariate

M

basic

pnat

basic

factors

intervals

prime

xgcd

polynomial

degree

card_pow_degree

definitions

lemmas

trailing_degree

algebra_map

basic

cancel_leads

coeff

denoms_clearable

derivative

div

erase_lead

eval

field_division

hasse_deriv

identities

induction

inductions

integral_normalization

iterated_deriv

lifts

mirror

monic

monomial

reverse

ring_division

taylor

qpf

multivariate

constructions

cofix

comp

const

fix

prj

quot

sigma

basic

univariate

basic

rat

basic

cast

default

denumerable

floor

meta_defs

order

sqrt

real

basic

cardinality

cau_seq

cau_seq_completion

conjugate_exponents

ennreal

ereal

golden_ratio

hyperreal

irrational

nnreal

pi

sign

sqrt

seq

computation

parallel

seq

wseq

set

intervals

basic

disjoint

image_preimage

infinite

ord_connected

pi

proj_Icc

surj_on

unordered_interval

Union_lift

accumulate

basic

bool

constructions

countable

enumerate

finite

function

lattice

pairwise

set_like

basic

fintype

setoid

basic

partition

sigma

basic

stream

basic

string

basic

defs

sym

basic

card

sym2

vector

basic

zmod

algebra

basic

parity

quotient

W

bool

bracket

bundle

char

dfinsupp

erased

fin

fin2

fin_enum

finmap

hash_map

holor

lazy_list

mllist

opposite

part

pequiv

pfun

pi

pprod

prod

quot

rel

semiquot

subtype

sum

tprod

tree

typevec

ulift

vector3

deprecated

group

ring

subfield

subgroup

submonoid

subring

dynamics

circle

rotation_number

translation_number

ergodic

conservative

measure_preserving

fixed_points

basic

topology

flow

omega_limit

periodic_pts

field_theory

finite

basic

galois_field

polynomial

abel_ruffini

adjoin

algebraic_closure

chevalley_warning

finiteness

fixed

galois

intermediate_field

minpoly

mv_polynomial

normal

perfect_closure

polynomial_galois_group

primitive_element

separable

separable_degree

splitting_field

subfield

tower

geometry

euclidean

basic

circumcenter

monge_point

sphere

triangle

manifold

algebra

left_invariant_derivation

lie_group

monoid

smooth_functions

structures

instances

real

sphere

units_of_normed_algebra

basic_smooth_bundle

bump_function

charted_space

conformal_groupoid

derivation_bundle

diffeomorph

local_invariant_properties

mfderiv

partition_of_unity

smooth_manifold_with_corners

times_cont_mdiff

times_cont_mdiff_map

whitney_embedding

group_theory

group_action

basic

defs

group

prod

sub_mul_action

units

perm

basic

concrete_cycle

cycle_type

cycles

fin

list

option

sign

subgroup

support

specific_groups

alternating

cyclic

dihedral

quaternion

submonoid

basic

center

membership

operations

abelianization

archimedean

complement

congruence

coset

eckmann_hilton

finiteness

free_abelian_group

free_abelian_group_finsupp

free_group

free_product

general_commutator

index

is_free_group

monoid_localization

nielsen_schreier

nilpotent

order_of_element

p_group

presented_group

quotient_group

semidirect_product

solvable

subgroup

sylow

linear_algebra

affine_space

affine_equiv

affine_map

affine_subspace

basic

combination

finite_dimensional

independent

midpoint

ordered

char_poly

basic

coeff

clifford_algebra

basic

conjugation

equivs

direct_sum

finsupp

tensor_product

matrix

absolute_value

basis

block

circulant

determinant

diagonal

dot_product

dual

finite_dimensional

is_diag

nonsingular_inverse

orthogonal

polynomial

reindex

symmetric

to_lin

to_linear_equiv

trace

transvection

adic_completion

alternating

basic

basis

bilinear_form

bilinear_map

coevaluation

contraction

determinant

dfinsupp

dimension

dual

eigenspace

exterior_algebra

finite_dimensional

finsupp

finsupp_vector_space

free_algebra

free_module

free_module_pid

invariant_basis_number

lagrange

linear_independent

linear_pmap

multilinear

pi

pi_tensor_product

prod

projection

quadratic_form

sesquilinear_form

smodeq

special_linear_group

std_basis

tensor_algebra

tensor_product

tensor_product_basis

trace

unitary_group

vandermonde

logic

function

basic

conjugate

iterate

basic

embedding

is_empty

nontrivial

relation

relator

small

unique

measure_theory

category

Meas

constructions

borel_space

pi

prod

decomposition

jordan

lebesgue

radon_nikodym

signed_hahn

unsigned_hahn

function

ae_eq_fun

ae_eq_of_integral

ae_measurable_sequence

conditional_expectation

continuous_map_dense

ess_sup

l1_space

l2_space

lp_space

simple_func_dense

special_functions

strongly_measurable

group

arithmetic

basic

prod

integral

bochner

integrable_on

integral_eq_improper

interval_integral

lebesgue

mean_inequalities

set_integral

set_to_l1

vitali_caratheodory

measure

content

giry_monad

haar

haar_lebesgue

hausdorff

lebesgue

measure_space

measure_space_def

outer_measure

regular

stieltjes

vector_measure

with_density_vector_measure

measurable_space

measurable_space_def

pi_system

probability_mass_function

tactic

category

LinearOrder

NonemptyFinLinOrd

PartialOrder

Preorder

omega_complete_partial_order

filter

archimedean

at_top_bot

bases

basic

cofinite

countable_Inter

ennreal

extr

filter_product

germ

indicator_function

interval

lift

partial

pointwise

ultrafilter

atoms

basic

boolean_algebra

bounded_lattice

bounds

closure

compactly_generated

complete_boolean_algebra

complete_lattice

conditionally_complete_lattice

copy

countable_dense_linear_order

directed

disjointed

extension

fixed_points

galois_connection

ideal

iterate

lattice

lattice_intervals

lexicographic

liminf_limsup

modular_lattice

omega_complete_partial_order

ord_continuous

order_dual

order_iso_nat

partial_sups

pfilter

pilex

preorder_hom

prime_ideal

rel_classes

rel_iso

semiconj_Sup

symm_diff

well_founded

well_founded_set

zorn

probability_theory

independence

integration

representation_theory

maschke

ring_theory

adjoin

basic

power_basis

ideal

basic

local_ring

operations

over

prod

int

basic

mv_polynomial

basic

polynomial

basic

bernstein

chebyshev

content

cyclotomic

dickson

gauss_lemma

homogeneous

pochhammer

rational_root

scale_roots

symmetric

tower

vieta

power_series

basic

well_known

valuation

basic

integers

integral

witt_vector

basic

compare

defs

frobenius

identities

init_tail

is_poly

mul_p

structure_polynomial

teichmuller

truncated

verschiebung

witt_polynomial

adjoin_root

algebra_tower

algebraic

artinian

class_group

coprime

dedekind_domain

derivation

discrete_valuation_ring

eisenstein_criterion

euclidean_domain

finiteness

fintype

flat

fractional_ideal

free_comm_ring

free_ring

hahn_series

integral_closure

integral_domain

integrally_closed

jacobson

jacobson_ideal

laurent_series

localization

matrix_algebra

multiplicity

nakayama

nilpotent

noetherian

non_zero_divisors

norm

nullstellensatz

perfection

polynomial_algebra

power_basis

prime

principal_ideal_domain

ring_invo

roots_of_unity

simple_module

subring

subsemiring

tensor_product

trace

unique_factorization_domain

set_theory

game

domineering

impartial

nim

short

state

winner

surreal

basic

dyadic

cardinal

cardinal_ordinal

cofinality

fincard

game

lists

ordinal

ordinal_arithmetic

ordinal_notation

pgame

schroeder_bernstein

zfc

system

random

basic

tactic

converter

apply_congr

binders

interactive

old_conv

linarith

datatypes

elimination

frontend

lemmas

parsing

preprocessing

verification

lint

basic

default

frontend

misc

simp

type_classes

monotonicity

basic

interactive

lemmas

nth_rewrite

basic

congr

default

omega

int

dnf

form

main

preterm

nat

dnf

form

main

neg_elim

preterm

sub_elim

clause

coeffs

eq_elim

find_ees

find_scalars

lin_comb

main

misc

prove_unsats

term

rewrite_all

basic

rewrite_search

discovery

explain

frontend

search

types

abel

algebra

alias

apply

apply_fun

auto_cases

binder_matching

cache

cancel_denoms

chain

choose

clear

congr

core

dec_trivial

delta_instance

dependencies

derive_fintype

derive_inhabited

doc_commands

elementwise

elide

equiv_rw

explode

explode_widget

ext

field_simp

fin_cases

find

find_unused

finish

fix_reflect_string

fresh_names

generalize_proofs

generalizes

group

has_variable_names

hint

induction

interactive

interactive_expr

interval_cases

itauto

lean_core_docs

lift

local_cache

localized

mk_iff_of_inductive_prop

noncomm_ring

norm_cast

norm_fin

norm_num

norm_swap

obviously

pi_instances

pretty_cases

protected

push_neg

rcases

reassoc_axiom

rename_var

replacer

reserved_notation

restate_axiom

rewrite

ring

ring2

ring_exp

scc

show_term

simp_command

simp_result

simp_rw

simpa

simps

slice

slim_check

solve_by_elim

split_ifs

squeeze

subtype_instance

suggest

tauto

tfae

tidy

transfer

transform_decl

transport

trunc_cases

unfold_cases

unify_equations

where

with_local_reducibility

wlog

zify

testing

slim_check

functions

gen

sampleable

testable

topology

algebra

nonarchimedean

basic

ordered

basic

extend_from

liminf_limsup

proj_Icc

affine

algebra

field

floor_ring

group

group_completion

group_with_zero

infinite_sum

localization

module

monoid

mul_action

multilinear

open_subgroup

polynomial

ring

uniform_field

uniform_group

uniform_ring

weak_dual_topology

category

CompHaus

default

projective

Profinite

as_limit

cofiltered_limit

default

projective

Top

adjunctions

basic

epi_mono

limits

open_nhds

opens

Compactum

TopCommRing

UniformSpace

continuous_function

algebra

basic

bounded

compact

polynomial

stone_weierstrass

weierstrass

instances

ennreal

ereal

nnreal

real

real_vector_space

locally_constant

algebra

basic

metric_space

algebra

antilipschitz

baire

basic

cau_seq_filter

closeds

completion

contracting

emetric_paracompact

emetric_space

gluing

gromov_hausdorff

gromov_hausdorff_realized

hausdorff_distance

holder

isometry

kuratowski

lipschitz

metric_separated

shrinking_lemma

sheaves

sheaf_condition

equalizer_products

opens_le_cover

pairwise_intersections

unique_gluing

forget

limits

local_predicate

presheaf

presheaf_of_functions

sheaf

sheaf_of_functions

sheafify

stalks

uniform_space

absolute_value

abstract_completion

basic

cauchy

compact_separated

compare_reals

complete_separated

completion

pi

separation

uniform_convergence

uniform_embedding

G_delta

alexandroff

bases

basic

compact_open

compacts

connected

constructions

continuous_on

dense_embedding

discrete_quotient

extend_from

fiber_bundle

homeomorph

homotopy

list

local_extr

local_homeomorph

maps

omega_complete_partial_order

opens

order

paracompact

partition_of_unity

path_connected

semicontinuous

separation

sequences

shrinking_lemma

stone_cech

subset_properties

tactic

unit_interval

urysohns_lemma

vector_bundle