mathlib
documentation
core
/
init
.
default
Google site search
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
index
tactics
commands
hole commands
attributes
notes
references
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
meta
converter
conv
interactive
lean
parser
smt
congruence_closure
ematch
interactive
rsimp
smt_tactic
widget
basic
html_cmd
interactive_expr
replace_save_info
tactic_component
ac_tactics
async_tactic
attribute
backward
case_tag
comp_value_tactics
congr_lemma
congr_tactic
constructor_tactic
contradiction_tactic
declaration
derive
environment
exceptional
expr
expr_address
float
format
fun_info
has_reflect
hole_command
injection_tactic
interaction_monad
interactive
interactive_base
json
level
local_context
match_tactic
mk_dec_eq_instance
mk_has_reflect_instance
mk_has_sizeof_instance
mk_inhabited_instance
module_info
name
occurrences
options
pexpr
rb_map
rec_util
ref
relation_tactics
rewrite_tactic
set_get_option_tactics
simp_tactic
tactic
tagged_format
task
type_context
vm
well_founded_tactics
cc_lemmas
classical
coe
core
default
function
funext
ite_simp
logic
propext
util
version
wf
system
io
io_interface
random
mathlib
algebra
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
meta
coinductive_predicates
expr
expr_lens
rb_map
uchange
number_theory
ADE_inequality
arithmetic_function
basic
bernoulli
bernoulli_polynomials
dioph
divisors
fermat4
lucas_lehmer
pell
primes_congruent_one
primorial
pythagorean_triples
quadratic_reciprocity
sum_four_squares
sum_two_squares
order
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