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