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.lazy_list
data.stream
system.io
system.io_interface
system.random
algebra.add_torsor
algebra.algebra.basic
algebra.algebra.operations
algebra.algebra.ordered
algebra.algebra.subalgebra
algebra.algebra.tower
algebra.archimedean
algebra.associated
algebra.big_operators.basic
algebra.big_operators.enat
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.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.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.kernels
algebra.category.Module.limits
algebra.category.Module.monoidal
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.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.direct_limit
algebra.direct_sum
algebra.direct_sum_graded
algebra.divisibility
algebra.euclidean_domain
algebra.field
algebra.field_power
algebra.floor
algebra.free
algebra.free_algebra
algebra.free_monoid
algebra.gcd_monoid
algebra.geom_sum
algebra.group.basic
algebra.group.commute
algebra.group.conj
algebra.group.default
algebra.group.defs
algebra.group.hom
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_ring_action
algebra.group_with_zero.basic
algebra.group_with_zero.defs
algebra.group_with_zero.power
algebra.homology.chain_complex
algebra.homology.exact
algebra.homology.homology
algebra.homology.image_to_kernel_map
algebra.invertible
algebra.iterate_hom
algebra.lie.abelian
algebra.lie.basic
algebra.lie.cartan_subalgebra
algebra.lie.classical
algebra.lie.direct_sum
algebra.lie.ideal_operations
algebra.lie.matrix
algebra.lie.nilpotent
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.universal_enveloping
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.submodule
algebra.module.submodule_lattice
algebra.module.ulift
algebra.monoid_algebra
algebra.opposites
algebra.order
algebra.order_functions
algebra.ordered_field
algebra.ordered_group
algebra.ordered_monoid
algebra.ordered_pi
algebra.ordered_ring
algebra.pempty_instances
algebra.pointwise
algebra.polynomial.big_operators
algebra.polynomial.group_ring_action
algebra.punit_instances
algebra.quadratic_discriminant
algebra.quandle
algebra.regular
algebra.ring.basic
algebra.ring.boolean_ring
algebra.ring.default
algebra.ring.pi
algebra.ring.prod
algebra.ring.ulift
algebra.ring_quot
algebra.smul_regular
algebra.smul_with_zero
algebra.squarefree
algebra.star.algebra
algebra.star.basic
algebra.star.chsh
algebra.triv_sq_zero_ext
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.simplex_category
algebraic_topology.simplicial_object
algebraic_topology.simplicial_set
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.darboux
analysis.calculus.deriv
analysis.calculus.extend_deriv
analysis.calculus.fderiv
analysis.calculus.fderiv_measurable
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.specific_functions
analysis.calculus.tangent_cone
analysis.calculus.times_cont_diff
analysis.complex.basic
analysis.complex.polynomial
analysis.complex.real_deriv
analysis.complex.roots_of_unity
analysis.convex.basic
analysis.convex.caratheodory
analysis.convex.cone
analysis.convex.extrema
analysis.convex.integral
analysis.convex.specific_functions
analysis.convex.topology
analysis.hofer
analysis.mean_inequalities
analysis.normed_space.add_torsor
analysis.normed_space.banach
analysis.normed_space.basic
analysis.normed_space.bounded_linear_maps
analysis.normed_space.complemented
analysis.normed_space.dual
analysis.normed_space.enorm
analysis.normed_space.euclidean_dist
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.linear_isometry
analysis.normed_space.mazur_ulam
analysis.normed_space.multilinear
analysis.normed_space.normed_group_hom
analysis.normed_space.operator_norm
analysis.normed_space.ordered
analysis.normed_space.riesz_lemma
analysis.normed_space.units
analysis.p_series
analysis.quaternion
analysis.seminorm
analysis.special_functions.arsinh
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.non_preadditive
category_theory.abelian.pseudoelements
category_theory.action
category_theory.additive.basic
category_theory.adjunction.basic
category_theory.adjunction.fully_faithful
category_theory.adjunction.lifting
category_theory.adjunction.limits
category_theory.adjunction.mates
category_theory.adjunction.opposites
category_theory.adjunction.reflective
category_theory.arrow
category_theory.category.Cat
category_theory.category.Groupoid
category_theory.category.Kleisli
category_theory.category.Rel
category_theory.category.default
category_theory.category.pairwise
category_theory.category.ulift
category_theory.closed.cartesian
category_theory.closed.functor
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.differential_object
category_theory.discrete_category
category_theory.elements
category_theory.endomorphism
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.cofinal
category_theory.limits.colimit_limit
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.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.creates
category_theory.limits.filtered_colimit_commutes_finite_limit
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.constructions.finite_products_of_binary_products
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.strong_epi
category_theory.limits.shapes.terminal
category_theory.limits.shapes.types
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.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.discrete
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.skeleton
category_theory.monoidal.transport
category_theory.monoidal.types
category_theory.natural_isomorphism
category_theory.natural_transformation
category_theory.opposites
category_theory.over
category_theory.pempty
category_theory.pi.basic
category_theory.preadditive.additive_functor
category_theory.preadditive.biproducts
category_theory.preadditive.default
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_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.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.rotate
category_theory.types
category_theory.whiskering
category_theory.with_terminal
category_theory.yoneda
combinatorics.colex
combinatorics.composition
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
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.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.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.encodable.basic
data.equiv.encodable.lattice
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.fincard
data.finmap
data.finset.basic
data.finset.fold
data.finset.gcd
data.finset.intervals
data.finset.lattice
data.finset.nat_antidiagonal
data.finset.order
data.finset.pi
data.finset.powerset
data.finset.preimage
data.finset.sort
data.finsupp.basic
data.finsupp.default
data.finsupp.lattice
data.finsupp.pointwise
data.fintype.basic
data.fintype.card
data.fintype.intervals
data.fintype.sort
data.fp.basic
data.hash_map
data.holor
data.indicator_function
data.int.basic
data.int.cast
data.int.char_zero
data.int.gcd
data.int.modeq
data.int.nat_prime
data.int.parity
data.int.range
data.int.sqrt
data.lazy_list.basic
data.list.alist
data.list.bag_inter
data.list.basic
data.list.chain
data.list.defs
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.tfae
data.list.zip
data.matrix.basic
data.matrix.char_p
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.gcd
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.digits
data.nat.dist
data.nat.enat
data.nat.factorial
data.nat.fib
data.nat.gcd
data.nat.log
data.nat.modeq
data.nat.multiplicity
data.nat.pairing
data.nat.parity
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.padics.hensel
data.padics.padic_integers
data.padics.padic_norm
data.padics.padic_numbers
data.padics.ring_homs
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.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.identities
data.polynomial.induction
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.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.quaternion
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.liouville
data.real.nnreal
data.real.pi
data.real.sqrt
data.rel
data.semiquot
data.seq.computation
data.seq.parallel
data.seq.seq
data.seq.wseq
data.set.accumulate
data.set.basic
data.set.constructions
data.set.countable
data.set.disjointed
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_like
data.setoid.basic
data.setoid.partition
data.sigma.basic
data.stream.basic
data.string.basic
data.string.defs
data.subtype
data.sum
data.support
data.sym
data.sym2
data.tprod
data.tree
data.typevec
data.ulift
data.vector2
data.zmod.basic
data.zmod.parity
data.zsqrtd.basic
data.zsqrtd.gaussian_int
data.zsqrtd.to_real
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.polynomial
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.splitting_field
field_theory.subfield
field_theory.tower
geometry.euclidean.basic
geometry.euclidean.circumcenter
geometry.euclidean.monge_point
geometry.euclidean.triangle
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.diffeomorph
geometry.manifold.instances.circle
geometry.manifold.instances.real
geometry.manifold.instances.sphere
geometry.manifold.local_invariant_properties
geometry.manifold.mfderiv
geometry.manifold.smooth_manifold_with_corners
geometry.manifold.times_cont_mdiff
geometry.manifold.times_cont_mdiff_map
group_theory.abelianization
group_theory.archimedean
group_theory.congruence
group_theory.coset
group_theory.eckmann_hilton
group_theory.free_abelian_group
group_theory.free_group
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.is_free_group
group_theory.monoid_localization
group_theory.order_of_element
group_theory.perm.basic
group_theory.perm.cycles
group_theory.perm.fin
group_theory.perm.option
group_theory.perm.sign
group_theory.perm.subgroup
group_theory.presented_group
group_theory.quotient_group
group_theory.semidirect_product
group_theory.solvable
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.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.char_poly.basic
linear_algebra.char_poly.coeff
linear_algebra.clifford_algebra.basic
linear_algebra.clifford_algebra.conjugation
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.direct_sum_module
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.invariant_basis_number
linear_algebra.lagrange
linear_algebra.linear_independent
linear_algebra.linear_pmap
linear_algebra.matrix
linear_algebra.multilinear
linear_algebra.nonsingular_inverse
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.unitary_group
logic.basic
logic.embedding
logic.function.basic
logic.function.conjugate
logic.function.iterate
logic.girard
logic.nontrivial
logic.relation
logic.relator
logic.small
logic.unique
measure_theory.ae_eq_fun
measure_theory.ae_eq_fun_metric
measure_theory.ae_measurable_sequence
measure_theory.arithmetic
measure_theory.bochner_integration
measure_theory.borel_space
measure_theory.category.Meas
measure_theory.content
measure_theory.decomposition
measure_theory.ess_sup
measure_theory.giry_monad
measure_theory.group
measure_theory.haar_measure
measure_theory.hausdorff_measure
measure_theory.integration
measure_theory.interval_integral
measure_theory.l1_space
measure_theory.l2_space
measure_theory.lebesgue_measure
measure_theory.lp_space
measure_theory.measurable_space
measure_theory.measure_space
measure_theory.outer_measure
measure_theory.pi
measure_theory.pi_system
measure_theory.probability_mass_function
measure_theory.prod
measure_theory.prod_group
measure_theory.set_integral
measure_theory.simple_func_dense
meta.coinductive_predicates
meta.expr
meta.expr_lens
meta.rb_map
meta.uchange
number_theory.ADE_inequality
number_theory.arithmetic_function
number_theory.basic
number_theory.bernoulli
number_theory.bernoulli_polynomials
number_theory.dioph
number_theory.divisors
number_theory.fermat4
number_theory.lucas_lehmer
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
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.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.pfilter
order.pilex
order.preorder_hom
order.prime_ideal
order.rel_classes
order.rel_iso
order.semiconj_Sup
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.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.operations
ring_theory.ideal.over
ring_theory.ideal.prod
ring_theory.int.basic
ring_theory.integral_closure
ring_theory.integral_domain
ring_theory.jacobson
ring_theory.jacobson_ideal
ring_theory.localization
ring_theory.matrix_algebra
ring_theory.multiplicity
ring_theory.mv_polynomial.basic
ring_theory.noetherian
ring_theory.non_zero_divisors
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.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
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.algebra.affine
topology.algebra.algebra
topology.algebra.floor_ring
topology.algebra.group
topology.algebra.group_completion
topology.algebra.group_with_zero
topology.algebra.infinite_sum
topology.algebra.module
topology.algebra.monoid
topology.algebra.mul_action
topology.algebra.multilinear
topology.algebra.nonarchimedean.basic
topology.algebra.normed_group
topology.algebra.open_subgroup
topology.algebra.ordered
topology.algebra.ordered.proj_Icc
topology.algebra.polynomial
topology.algebra.ring
topology.algebra.uniform_group
topology.algebra.uniform_ring
topology.bases
topology.basic
topology.category.CompHaus
topology.category.Compactum
topology.category.Profinite
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_on
topology.dense_embedding
topology.extend_from_subset
topology.homeomorph
topology.instances.ennreal
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.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_space
topology.metric_space.gluing
topology.metric_space.gromov_hausdorff
topology.metric_space.gromov_hausdorff_realized
topology.metric_space.hausdorff_distance
topology.metric_space.isometry
topology.metric_space.kuratowski
topology.metric_space.lipschitz
topology.metric_space.metric_separated
topology.metric_space.pi_Lp
topology.omega_complete_partial_order
topology.opens
topology.order
topology.paracompact
topology.path_connected
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.topological_fiber_bundle
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

lazy_list

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

subalgebra

tower

big_operators

basic

enat

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

kernels

limits

monoidal

subobject

Mon

adjunctions

basic

colimits

limits

Semigroup

basic

char_p

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

group

basic

commute

conj

default

defs

hom

inj_surj

pi

prod

semiconj

to_additive

type_tags

ulift

units

units_hom

with_one

group_power

basic

identities

lemmas

group_with_zero

basic

defs

power

homology

chain_complex

exact

homology

image_to_kernel_map

lie

abelian

basic

cartan_subalgebra

classical

direct_sum

ideal_operations

matrix

nilpotent

of_associative

quotient

semisimple

skew_adjoint

solvable

subalgebra

submodule

universal_enveloping

module

basic

default

hom

linear_map

opposites

ordered

pi

prod

submodule

submodule_lattice

ulift

polynomial

big_operators

group_ring_action

ring

basic

boolean_ring

default

pi

prod

ulift

star

algebra

basic

chsh

add_torsor

archimedean

associated

char_zero

direct_limit

direct_sum

direct_sum_graded

divisibility

euclidean_domain

field

field_power

floor

free

free_algebra

free_monoid

gcd_monoid

geom_sum

group_action_hom

group_ring_action

invertible

iterate_hom

linear_ordered_comm_group_with_zero

linear_recurrence

monoid_algebra

opposites

order

order_functions

ordered_field

ordered_group

ordered_monoid

ordered_pi

ordered_ring

pempty_instances

pointwise

punit_instances

quadratic_discriminant

quandle

regular

ring_quot

smul_regular

smul_with_zero

squarefree

triv_sq_zero_ext

algebraic_geometry

presheafed_space

has_colimits

Scheme

Spec

is_open_comap_C

locally_ringed_space

presheafed_space

prime_spectrum

sheafed_space

stalks

structure_sheaf

algebraic_topology

simplex_category

simplicial_object

simplicial_set

analysis

ODE

gronwall

analytic

basic

composition

inverse

linear

radius_liminf

asymptotics

asymptotic_equivalent

asymptotics

specific_asymptotics

calculus

darboux

deriv

extend_deriv

fderiv

fderiv_measurable

formal_multilinear_series

implicit

inverse

iterated_deriv

lagrange_multipliers

lhopital

local_extr

mean_value

specific_functions

tangent_cone

times_cont_diff

complex

basic

polynomial

real_deriv

roots_of_unity

convex

basic

caratheodory

cone

extrema

integral

specific_functions

topology

normed_space

add_torsor

banach

basic

bounded_linear_maps

complemented

dual

enorm

euclidean_dist

extend

finite_dimension

hahn_banach

indicator_function

inner_product

linear_isometry

mazur_ulam

multilinear

normed_group_hom

operator_norm

ordered

riesz_lemma

units

special_functions

arsinh

exp_log

integrals

polynomials

pow

sqrt

trigonometric

hofer

mean_inequalities

p_series

quaternion

seminorm

specific_limits

category_theory

abelian

diagram_lemmas

four

basic

exact

non_preadditive

pseudoelements

additive

basic

adjunction

basic

fully_faithful

lifting

limits

mates

opposites

reflective

category

Cat

Groupoid

Kleisli

Rel

default

pairwise

ulift

closed

cartesian

functor

monoidal

types

zero

concrete_category

basic

bundled

bundled_hom

reflects_isomorphisms

unbundled_hom

limits

constructions

over

connected

default

products

binary_products

epi_mono

equalizers

limits_of_products_and_equalizers

pullbacks

preserves

shapes

binary_products

equalizers

products

pullbacks

terminal

basic

functor_category

limits

shapes

constructions

finite_products_of_binary_products

binary_products

biproducts

concrete_category

equalizers

finite_limits

finite_products

images

kernel_pair

kernels

normal_mono

products

pullbacks

reflexive

regular_mono

split_coequalizer

strong_epi

terminal

types

wide_pullbacks

zero

cofinal

colimit_limit

concrete_category

cones

connected

creates

filtered_colimit_commutes_finite_limit

fubini

functor_category

has_limits

is_limit

kan_extension

lattice

opposites

over

pi

presheaf

punit

small_complete

types

yoneda

monad

adjunction

algebra

basic

coequalizer

equiv_mon

kleisli

limits

monadicity

products

types

monoidal

internal

Module

functor_category

limits

types

CommMon_

End

Mod

Mon_

braided

category

discrete

functor

functor_category

functorial

limits

natural_transformation

of_chosen_finite_products

of_has_finite_products

skeleton

transport

types

pi

basic

preadditive

additive_functor

biproducts

default

schur

single_obj

products

associator

basic

bifunctor

sigma

basic

sites

canonical

closed

grothendieck

pretopology

sheaf_of_types

sieves

spaces

types

subobject

basic

factor_thru

lattice

mono_over

types

well_powered

sums

associator

basic

triangulated

basic

rotate

Fintype

action

arrow

comma

conj

connected_components

const

core

currying

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

pempty

punit

quotient

reflects_isomorphisms

shift

simple

single_obj

skeletal

structured_arrow

subterminal

thin

types

whiskering

with_terminal

yoneda

combinatorics

simple_graph

adj_matrix

basic

degree_sum

matching

strongly_regular

colex

composition

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

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

basic

denumerable

fin

fintype

functor

list

local_equiv

mul_add

mul_add_aut

nat

option

ring

ring_aut

transfer_instance

finset

basic

fold

gcd

intervals

lattice

nat_antidiagonal

order

pi

powerset

preimage

sort

finsupp

basic

default

lattice

pointwise

fintype

basic

card

intervals

sort

fp

basic

int

basic

cast

char_zero

gcd

modeq

nat_prime

parity

range

sqrt

lazy_list

basic

list

alist

bag_inter

basic

chain

defs

erase_dup

forall2

func

indexes

intervals

min_max

nat_antidiagonal

nodup

nodup_equiv_fin

of_fn

pairwise

palindrome

perm

range

rotate

sections

sigma

sort

tfae

zip

matrix

basic

char_p

notation

pequiv

multiset

antidiagonal

basic

erase_dup

finset_ops

fold

functor

gcd

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

basic

bitwise

cast

digits

dist

enat

factorial

fib

gcd

log

modeq

multiplicity

pairing

parity

prime

psub

sqrt

totient

upto

with_bot

num

basic

bitwise

lemmas

prime

option

basic

defs

ordmap

ordnode

ordset

padics

hensel

padic_integers

padic_norm

padic_numbers

ring_homs

pfunctor

multivariate

M

W

basic

univariate

M

basic

pnat

basic

factors

intervals

prime

xgcd

polynomial

degree

definitions

lemmas

trailing_degree

algebra_map

basic

cancel_leads

coeff

denoms_clearable

derivative

div

erase_lead

eval

field_division

identities

induction

integral_normalization

iterated_deriv

lifts

mirror

monic

monomial

reverse

ring_division

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

liouville

nnreal

pi

sqrt

seq

computation

parallel

seq

wseq

set

intervals

basic

disjoint

image_preimage

infinite

ord_connected

pi

proj_Icc

surj_on

unordered_interval

accumulate

basic

constructions

countable

disjointed

enumerate

finite

function

lattice

setoid

basic

partition

sigma

basic

stream

basic

string

basic

defs

zmod

basic

parity

zsqrtd

basic

gaussian_int

to_real

W

bool

bracket

char

dfinsupp

erased

fin

fin2

fin_enum

fincard

finmap

hash_map

holor

indicator_function

mllist

opposite

pequiv

pfun

pi

pprod

prod

quaternion

quot

rel

semiquot

set_like

subtype

sum

support

sym

sym2

tprod

tree

typevec

ulift

vector2

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

polynomial

abel_ruffini

adjoin

algebraic_closure

chevalley_warning

fixed

galois

intermediate_field

minpoly

mv_polynomial

normal

perfect_closure

polynomial_galois_group

primitive_element

separable

splitting_field

subfield

tower

geometry

euclidean

basic

circumcenter

monge_point

triangle

manifold

algebra

lie_group

monoid

smooth_functions

structures

instances

circle

real

sphere

basic_smooth_bundle

bump_function

charted_space

diffeomorph

local_invariant_properties

mfderiv

smooth_manifold_with_corners

times_cont_mdiff

times_cont_mdiff_map

group_theory

group_action

basic

defs

group

prod

sub_mul_action

perm

basic

cycles

fin

option

sign

subgroup

specific_groups

cyclic

dihedral

quaternion

submonoid

basic

membership

operations

abelianization

archimedean

congruence

coset

eckmann_hilton

free_abelian_group

free_group

is_free_group

monoid_localization

order_of_element

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

direct_sum

finsupp

tensor_product

adic_completion

alternating

basic

basis

bilinear_form

contraction

determinant

dfinsupp

dimension

direct_sum_module

dual

eigenspace

exterior_algebra

finite_dimensional

finsupp

finsupp_vector_space

free_algebra

free_module

invariant_basis_number

lagrange

linear_independent

linear_pmap

matrix

multilinear

nonsingular_inverse

pi

pi_tensor_product

prod

projection

quadratic_form

sesquilinear_form

smodeq

special_linear_group

std_basis

tensor_algebra

tensor_product

unitary_group

logic

function

basic

conjugate

iterate

basic

embedding

girard

nontrivial

relation

relator

small

unique

measure_theory

category

Meas

ae_eq_fun

ae_eq_fun_metric

ae_measurable_sequence

arithmetic

bochner_integration

borel_space

content

decomposition

ess_sup

giry_monad

group

haar_measure

hausdorff_measure

integration

interval_integral

l1_space

l2_space

lebesgue_measure

lp_space

measurable_space

measure_space

outer_measure

pi

pi_system

probability_mass_function

prod

prod_group

set_integral

simple_func_dense

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

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

pfilter

pilex

preorder_hom

prime_ideal

rel_classes

rel_iso

semiconj_Sup

well_founded

well_founded_set

zorn

probability_theory

independence

integration

representation_theory

maschke

ring_theory

adjoin

basic

power_basis

ideal

basic

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

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

jacobson

jacobson_ideal

localization

matrix_algebra

multiplicity

noetherian

non_zero_divisors

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

cardinal

cardinal_ordinal

cofinality

game

lists

ordinal

ordinal_arithmetic

ordinal_notation

pgame

schroeder_bernstein

surreal

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

proj_Icc

affine

algebra

floor_ring

group

group_completion

group_with_zero

infinite_sum

module

monoid

mul_action

multilinear

normed_group

open_subgroup

ordered

polynomial

ring

uniform_group

uniform_ring

category

Top

adjunctions

basic

epi_mono

limits

open_nhds

opens

CompHaus

Compactum

Profinite

TopCommRing

UniformSpace

continuous_function

algebra

basic

bounded

compact

instances

ennreal

nnreal

real

real_vector_space

locally_constant

algebra

basic

metric_space

antilipschitz

baire

basic

cau_seq_filter

closeds

completion

contracting

emetric_space

gluing

gromov_hausdorff

gromov_hausdorff_realized

hausdorff_distance

isometry

kuratowski

lipschitz

metric_separated

pi_Lp

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

bases

basic

compact_open

compacts

connected

constructions

continuous_on

dense_embedding

extend_from_subset

homeomorph

list

local_extr

local_homeomorph

maps

omega_complete_partial_order

opens

order

paracompact

path_connected

separation

sequences

shrinking_lemma

stone_cech

subset_properties

tactic

topological_fiber_bundle

unit_interval

urysohns_lemma

vector_bundle