mathlib3
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.feature_search
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
examples.recursors
for_mathlib.algebra.algebra.opposite
for_mathlib.algebra.algebra_operations
for_mathlib.algebra.center_submonoid
for_mathlib.algebra.filtration
for_mathlib.algebra.monoid_algebra
for_mathlib.algebra.ring_quot
for_mathlib.linear_algebra.bilinear_form.basic
for_mathlib.linear_algebra.bilinear_form.tensor_product
for_mathlib.linear_algebra.quadratic_form.isometric_map
for_mathlib.linear_algebra.quadratic_form.prod
for_mathlib.linear_algebra.tensor_product
for_mathlib.linear_algebra.tensor_product.inner_product_space
for_mathlib.linear_algebra.tensor_product.opposite
for_mathlib.ring_theory.tensor_product
geometric_algebra.from_mathlib.basic
geometric_algebra.from_mathlib.category_theory
geometric_algebra.from_mathlib.complexification
geometric_algebra.from_mathlib.concrete.cga
geometric_algebra.from_mathlib.concrete.default
geometric_algebra.from_mathlib.concrete.pga
geometric_algebra.from_mathlib.conjugation
geometric_algebra.from_mathlib.contract
geometric_algebra.from_mathlib.default
geometric_algebra.from_mathlib.even_odd
geometric_algebra.from_mathlib.even_odd_equiv
geometric_algebra.from_mathlib.fold
geometric_algebra.from_mathlib.mathoverflow
geometric_algebra.from_mathlib.versors
geometric_algebra.from_mathlib.zmod_grading
geometric_algebra.nursery.chisolm
geometric_algebra.nursery.graded
geometric_algebra.nursery.instances
geometric_algebra.translations.hol_light
geometric_algebra.translations.ida
geometric_algebra.translations.ida_derived
geometric_algebra.translations.laurents
algebra.abs
algebra.add_torsor
algebra.algebra.basic
algebra.algebra.bilinear
algebra.algebra.equiv
algebra.algebra.hom
algebra.algebra.operations
algebra.algebra.pi
algebra.algebra.prod
algebra.algebra.restrict_scalars
algebra.algebra.subalgebra.basic
algebra.algebra.subalgebra.tower
algebra.algebra.tower
algebra.associated
algebra.big_operators.associated
algebra.big_operators.basic
algebra.big_operators.fin
algebra.big_operators.finprod
algebra.big_operators.finsupp
algebra.big_operators.intervals
algebra.big_operators.multiset.basic
algebra.big_operators.multiset.lemmas
algebra.big_operators.nat_antidiagonal
algebra.big_operators.option
algebra.big_operators.order
algebra.big_operators.pi
algebra.big_operators.ring
algebra.big_operators.ring_equiv
algebra.bounds
algebra.category.Algebra.basic
algebra.category.Group.basic
algebra.category.Group.preadditive
algebra.category.Module.basic
algebra.category.Mon.basic
algebra.category.Ring.basic
algebra.char_p.algebra
algebra.char_p.basic
algebra.char_p.invertible
algebra.char_p.pi
algebra.char_p.quotient
algebra.char_p.two
algebra.char_zero.defs
algebra.char_zero.infinite
algebra.char_zero.lemmas
algebra.covariant_and_contravariant
algebra.direct_sum.algebra
algebra.direct_sum.basic
algebra.direct_sum.decomposition
algebra.direct_sum.finsupp
algebra.direct_sum.internal
algebra.direct_sum.module
algebra.direct_sum.ring
algebra.divisibility.basic
algebra.divisibility.units
algebra.dual_number
algebra.euclidean_domain.basic
algebra.euclidean_domain.defs
algebra.euclidean_domain.instances
algebra.field.basic
algebra.field.defs
algebra.field.opposite
algebra.free_algebra
algebra.free_monoid.basic
algebra.gcd_monoid.basic
algebra.gcd_monoid.finset
algebra.gcd_monoid.multiset
algebra.geom_sum
algebra.graded_monoid
algebra.group.basic
algebra.group.commutator
algebra.group.commute
algebra.group.conj
algebra.group.defs
algebra.group.ext
algebra.group.inj_surj
algebra.group.opposite
algebra.group.order_synonym
algebra.group.pi
algebra.group.prod
algebra.group.semiconj
algebra.group.type_tags
algebra.group.ulift
algebra.group.units
algebra.group.with_one.defs
algebra.group_power.basic
algebra.group_power.lemmas
algebra.group_power.order
algebra.group_power.ring
algebra.group_ring_action.basic
algebra.group_ring_action.subobjects
algebra.group_with_zero.basic
algebra.group_with_zero.commute
algebra.group_with_zero.defs
algebra.group_with_zero.divisibility
algebra.group_with_zero.inj_surj
algebra.group_with_zero.power
algebra.group_with_zero.semiconj
algebra.group_with_zero.units.basic
algebra.group_with_zero.units.lemmas
algebra.hom.aut
algebra.hom.commute
algebra.hom.embedding
algebra.hom.equiv.basic
algebra.hom.equiv.units.basic
algebra.hom.equiv.units.group_with_zero
algebra.hom.group
algebra.hom.group_action
algebra.hom.group_instances
algebra.hom.iterate
algebra.hom.non_unital_alg
algebra.hom.ring
algebra.hom.units
algebra.indicator_function
algebra.invertible
algebra.module.algebra
algebra.module.basic
algebra.module.big_operators
algebra.module.equiv
algebra.module.hom
algebra.module.linear_map
algebra.module.opposites
algebra.module.pi
algebra.module.prod
algebra.module.submodule.basic
algebra.module.submodule.bilinear
algebra.module.submodule.lattice
algebra.module.submodule.pointwise
algebra.module.ulift
algebra.monoid_algebra.basic
algebra.monoid_algebra.division
algebra.monoid_algebra.ideal
algebra.monoid_algebra.support
algebra.ne_zero
algebra.opposites
algebra.order.absolute_value
algebra.order.archimedean
algebra.order.field.basic
algebra.order.field.canonical.basic
algebra.order.field.canonical.defs
algebra.order.field.defs
algebra.order.field.inj_surj
algebra.order.field.power
algebra.order.floor
algebra.order.group.abs
algebra.order.group.bounds
algebra.order.group.defs
algebra.order.group.inj_surj
algebra.order.group.instances
algebra.order.group.min_max
algebra.order.group.order_iso
algebra.order.group.type_tags
algebra.order.group.units
algebra.order.hom.basic
algebra.order.invertible
algebra.order.kleene
algebra.order.module
algebra.order.monoid.basic
algebra.order.monoid.cancel.basic
algebra.order.monoid.cancel.defs
algebra.order.monoid.canonical.defs
algebra.order.monoid.defs
algebra.order.monoid.lemmas
algebra.order.monoid.min_max
algebra.order.monoid.nat_cast
algebra.order.monoid.order_dual
algebra.order.monoid.prod
algebra.order.monoid.type_tags
algebra.order.monoid.units
algebra.order.monoid.with_top
algebra.order.monoid.with_zero.basic
algebra.order.monoid.with_zero.defs
algebra.order.nonneg.field
algebra.order.nonneg.floor
algebra.order.nonneg.ring
algebra.order.pi
algebra.order.positive.ring
algebra.order.ring.abs
algebra.order.ring.canonical
algebra.order.ring.char_zero
algebra.order.ring.defs
algebra.order.ring.inj_surj
algebra.order.ring.lemmas
algebra.order.ring.with_top
algebra.order.smul
algebra.order.sub.canonical
algebra.order.sub.defs
algebra.order.sub.with_top
algebra.order.with_zero
algebra.order.zero_le_one
algebra.parity
algebra.periodic
algebra.polynomial.big_operators
algebra.punit_instances
algebra.quaternion
algebra.quaternion_basis
algebra.quotient
algebra.regular.basic
algebra.regular.smul
algebra.ring.aut
algebra.ring.basic
algebra.ring.commute
algebra.ring.comp_typeclasses
algebra.ring.defs
algebra.ring.divisibility
algebra.ring.equiv
algebra.ring.fin
algebra.ring.idempotents
algebra.ring.inj_surj
algebra.ring.opposite
algebra.ring.pi
algebra.ring.prod
algebra.ring.regular
algebra.ring.semiconj
algebra.ring.ulift
algebra.ring.units
algebra.ring_quot
algebra.smul_with_zero
algebra.star.basic
algebra.star.big_operators
algebra.star.module
algebra.star.order
algebra.star.pi
algebra.star.pointwise
algebra.star.prod
algebra.star.self_adjoint
algebra.star.star_alg_hom
algebra.star.subalgebra
algebra.star.unitary
algebra.support
algebra.triv_sq_zero_ext
analysis.asymptotics.asymptotics
analysis.complex.basic
analysis.convex.basic
analysis.convex.combination
analysis.convex.function
analysis.convex.hull
analysis.convex.jensen
analysis.convex.normed
analysis.convex.segment
analysis.convex.star
analysis.convex.strict
analysis.convex.strict_convex_space
analysis.convex.topology
analysis.convex.uniform
analysis.inner_product_space.basic
analysis.locally_convex.balanced_core_hull
analysis.locally_convex.basic
analysis.locally_convex.bounded
analysis.normed.field.basic
analysis.normed.group.add_torsor
analysis.normed.group.basic
analysis.normed.group.completion
analysis.normed.group.hom
analysis.normed.group.infinite_sum
analysis.normed.group.pointwise
analysis.normed.group.seminorm
analysis.normed.mul_action
analysis.normed.order.basic
analysis.normed_space.add_torsor
analysis.normed_space.affine_isometry
analysis.normed_space.basic
analysis.normed_space.bounded_linear_maps
analysis.normed_space.completion
analysis.normed_space.continuous_linear_map
analysis.normed_space.linear_isometry
analysis.normed_space.multilinear
analysis.normed_space.operator_norm
analysis.normed_space.pointwise
analysis.normed_space.ray
analysis.normed_space.star.basic
analysis.normed_space.units
analysis.seminorm
analysis.specific_limits.basic
analysis.specific_limits.normed
category_theory.adjunction.basic
category_theory.arrow
category_theory.balanced
category_theory.bicategory.basic
category_theory.bicategory.strict
category_theory.category.Cat
category_theory.category.basic
category_theory.category.preorder
category_theory.category.ulift
category_theory.comm_sq
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.conj
category_theory.discrete_category
category_theory.elementwise
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.fin_category
category_theory.full_subcategory
category_theory.functor.basic
category_theory.functor.category
category_theory.functor.const
category_theory.functor.currying
category_theory.functor.epi_mono
category_theory.functor.fully_faithful
category_theory.functor.hom
category_theory.functor.reflects_isomorphisms
category_theory.groupoid
category_theory.isomorphism
category_theory.isomorphism_classes
category_theory.lifting_properties.adjunction
category_theory.lifting_properties.basic
category_theory.limits.cones
category_theory.limits.constructions.epi_mono
category_theory.limits.exact_functor
category_theory.limits.has_limits
category_theory.limits.is_limit
category_theory.limits.preserves.basic
category_theory.limits.preserves.finite
category_theory.limits.preserves.shapes.binary_products
category_theory.limits.preserves.shapes.biproducts
category_theory.limits.preserves.shapes.products
category_theory.limits.preserves.shapes.pullbacks
category_theory.limits.preserves.shapes.terminal
category_theory.limits.preserves.shapes.zero
category_theory.limits.shapes.binary_products
category_theory.limits.shapes.biproducts
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.kernels
category_theory.limits.shapes.products
category_theory.limits.shapes.pullbacks
category_theory.limits.shapes.strong_epi
category_theory.limits.shapes.terminal
category_theory.limits.shapes.wide_pullbacks
category_theory.limits.shapes.zero_morphisms
category_theory.limits.shapes.zero_objects
category_theory.linear.basic
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.basic
category_theory.preadditive.biproducts
category_theory.preadditive.functor_category
category_theory.products.basic
category_theory.products.bifunctor
category_theory.punit
category_theory.skeletal
category_theory.structured_arrow
category_theory.thin
category_theory.types
category_theory.whiskering
category_theory.yoneda
combinatorics.composition
combinatorics.partition
combinatorics.quiver.basic
combinatorics.quiver.connected_component
combinatorics.quiver.path
combinatorics.quiver.push
combinatorics.quiver.subquiver
combinatorics.quiver.symmetric
control.applicative
control.basic
control.bifunctor
control.equiv_functor
control.equiv_functor.instances
control.functor
control.monad.basic
control.traversable.basic
control.traversable.derive
control.traversable.equiv
control.traversable.instances
control.traversable.lemmas
data.array.lemmas
data.bool.basic
data.bool.set
data.bracket
data.buffer.basic
data.buffer.parser.basic
data.buffer.parser.numeral
data.char
data.complex.basic
data.complex.exponential
data.complex.module
data.countable.basic
data.countable.defs
data.dfinsupp.basic
data.dlist.basic
data.enat.basic
data.enat.lattice
data.fin.basic
data.fin.interval
data.fin.tuple.basic
data.fin.vec_notation
data.finite.basic
data.finite.card
data.finite.defs
data.finite.set
data.finset.basic
data.finset.card
data.finset.fin
data.finset.fold
data.finset.image
data.finset.lattice
data.finset.locally_finite
data.finset.n_ary
data.finset.nat_antidiagonal
data.finset.noncomm_prod
data.finset.option
data.finset.order
data.finset.pairwise
data.finset.pi
data.finset.pointwise
data.finset.powerset
data.finset.preimage
data.finset.prod
data.finset.sigma
data.finset.sort
data.finset.sum
data.finsupp.antidiagonal
data.finsupp.basic
data.finsupp.defs
data.finsupp.fin
data.finsupp.indicator
data.finsupp.multiset
data.finsupp.order
data.finsupp.to_dfinsupp
data.fintype.basic
data.fintype.big_operators
data.fintype.card
data.fintype.fin
data.fintype.lattice
data.fintype.list
data.fintype.option
data.fintype.perm
data.fintype.pi
data.fintype.powerset
data.fintype.prod
data.fintype.sigma
data.fintype.sort
data.fintype.sum
data.fintype.units
data.fintype.vector
data.fun_like.basic
data.fun_like.embedding
data.fun_like.equiv
data.int.basic
data.int.bitwise
data.int.cast.basic
data.int.cast.defs
data.int.cast.field
data.int.cast.lemmas
data.int.cast.prod
data.int.char_zero
data.int.div
data.int.dvd.basic
data.int.gcd
data.int.interval
data.int.least_greatest
data.int.lemmas
data.int.modeq
data.int.order.basic
data.int.order.lemmas
data.int.order.units
data.int.parity
data.int.units
data.is_R_or_C.basic
data.json
data.list.basic
data.list.big_operators.basic
data.list.big_operators.lemmas
data.list.chain
data.list.count
data.list.cycle
data.list.dedup
data.list.defs
data.list.duplicate
data.list.fin_range
data.list.forall2
data.list.func
data.list.indexes
data.list.infix
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.prime
data.list.prod_sigma
data.list.range
data.list.rotate
data.list.sort
data.list.sublists
data.list.tfae
data.list.zip
data.matrix.basic
data.matrix.basis
data.matrix.block
data.matrix.invertible
data.matrix.notation
data.matrix.pequiv
data.mllist
data.multiset.antidiagonal
data.multiset.basic
data.multiset.bind
data.multiset.dedup
data.multiset.finset_ops
data.multiset.fold
data.multiset.lattice
data.multiset.nat_antidiagonal
data.multiset.nodup
data.multiset.pi
data.multiset.powerset
data.multiset.range
data.multiset.sort
data.multiset.sum
data.mv_polynomial.basic
data.mv_polynomial.comm_ring
data.mv_polynomial.division
data.mv_polynomial.equiv
data.mv_polynomial.rename
data.mv_polynomial.variables
data.nat.basic
data.nat.bits
data.nat.bitwise
data.nat.cast.basic
data.nat.cast.defs
data.nat.cast.field
data.nat.cast.prod
data.nat.choose.basic
data.nat.choose.sum
data.nat.digits
data.nat.factorial.basic
data.nat.factors
data.nat.gcd.basic
data.nat.interval
data.nat.lattice
data.nat.log
data.nat.modeq
data.nat.multiplicity
data.nat.order.basic
data.nat.order.lemmas
data.nat.pairing
data.nat.parity
data.nat.part_enat
data.nat.pow
data.nat.prime
data.nat.set
data.nat.size
data.nat.sqrt
data.nat.succ_pred
data.nat.units
data.nat.with_bot
data.num.basic
data.opposite
data.option.basic
data.option.defs
data.option.n_ary
data.part
data.pequiv
data.pi.algebra
data.pi.lex
data.pnat.basic
data.pnat.defs
data.pnat.interval
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.derivative
data.polynomial.div
data.polynomial.erase_lead
data.polynomial.eval
data.polynomial.field_division
data.polynomial.induction
data.polynomial.inductions
data.polynomial.monic
data.polynomial.monomial
data.polynomial.reverse
data.polynomial.ring_division
data.prod.basic
data.prod.lex
data.prod.pprod
data.quot
data.rat.basic
data.rat.big_operators
data.rat.cast
data.rat.defs
data.rat.floor
data.rat.init
data.rat.lemmas
data.rat.meta_defs
data.rat.order
data.rbmap.basic
data.rbtree.default_lt
data.rbtree.init
data.real.basic
data.real.cau_seq
data.real.cau_seq_completion
data.real.ennreal
data.real.nnreal
data.real.pointwise
data.real.sqrt
data.set.Union_lift
data.set.accumulate
data.set.basic
data.set.bool_indicator
data.set.countable
data.set.finite
data.set.function
data.set.functor
data.set.image
data.set.intervals.basic
data.set.intervals.disjoint
data.set.intervals.group
data.set.intervals.infinite
data.set.intervals.instances
data.set.intervals.monoid
data.set.intervals.ord_connected
data.set.intervals.order_iso
data.set.intervals.pi
data.set.intervals.proj_Icc
data.set.intervals.unordered_interval
data.set.lattice
data.set.list
data.set.n_ary
data.set.pairwise.basic
data.set.pairwise.lattice
data.set.pointwise.basic
data.set.pointwise.big_operators
data.set.pointwise.finite
data.set.pointwise.interval
data.set.pointwise.list_of_fn
data.set.pointwise.smul
data.set.prod
data.set.semiring
data.set.sigma
data.set_like.basic
data.setoid.basic
data.sigma.basic
data.sigma.lex
data.sign
data.string.basic
data.string.defs
data.subtype
data.sum.basic
data.sum.order
data.sym.basic
data.tree
data.ulift
data.vector.basic
data.zmod.basic
data.zmod.defs
dynamics.fixed_points.basic
dynamics.periodic_pts
field_theory.finiteness
field_theory.mv_polynomial
field_theory.subfield
field_theory.tower
group_theory.archimedean
group_theory.commutator
group_theory.congruence
group_theory.coset
group_theory.finiteness
group_theory.group_action.basic
group_theory.group_action.big_operators
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.quotient
group_theory.group_action.sub_mul_action
group_theory.group_action.sub_mul_action.pointwise
group_theory.group_action.units
group_theory.index
group_theory.monoid_localization
group_theory.order_of_element
group_theory.perm.basic
group_theory.perm.cycle.basic
group_theory.perm.cycle.type
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.quotient_group
group_theory.subgroup.actions
group_theory.subgroup.basic
group_theory.subgroup.finite
group_theory.subgroup.mul_opposite
group_theory.subgroup.pointwise
group_theory.subgroup.zpowers
group_theory.submonoid.basic
group_theory.submonoid.center
group_theory.submonoid.centralizer
group_theory.submonoid.membership
group_theory.submonoid.operations
group_theory.submonoid.pointwise
group_theory.subsemigroup.basic
group_theory.subsemigroup.center
group_theory.subsemigroup.centralizer
group_theory.subsemigroup.operations
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.independent
linear_algebra.affine_space.midpoint
linear_algebra.affine_space.midpoint_zero
linear_algebra.affine_space.restrict
linear_algebra.alternating
linear_algebra.basic
linear_algebra.basis
linear_algebra.basis.bilinear
linear_algebra.bilinear_form
linear_algebra.bilinear_form.tensor_product
linear_algebra.bilinear_map
linear_algebra.clifford_algebra.basic
linear_algebra.clifford_algebra.conjugation
linear_algebra.clifford_algebra.contraction
linear_algebra.clifford_algebra.equivs
linear_algebra.clifford_algebra.even
linear_algebra.clifford_algebra.even_equiv
linear_algebra.clifford_algebra.fold
linear_algebra.clifford_algebra.grading
linear_algebra.clifford_algebra.star
linear_algebra.dfinsupp
linear_algebra.dimension
linear_algebra.direct_sum.finsupp
linear_algebra.direct_sum.tensor_product
linear_algebra.dual
linear_algebra.exterior_algebra.basic
linear_algebra.finite_dimensional
linear_algebra.finrank
linear_algebra.finsupp
linear_algebra.finsupp_vector_space
linear_algebra.free_module.basic
linear_algebra.free_module.finite.basic
linear_algebra.free_module.finite.matrix
linear_algebra.free_module.finite.rank
linear_algebra.free_module.rank
linear_algebra.general_linear_group
linear_algebra.invariant_basis_number
linear_algebra.isomorphisms
linear_algebra.linear_independent
linear_algebra.linear_pmap
linear_algebra.matrix.adjugate
linear_algebra.matrix.basis
linear_algebra.matrix.bilinear_form
linear_algebra.matrix.determinant
linear_algebra.matrix.general_linear_group
linear_algebra.matrix.mv_polynomial
linear_algebra.matrix.nondegenerate
linear_algebra.matrix.nonsingular_inverse
linear_algebra.matrix.polynomial
linear_algebra.matrix.reindex
linear_algebra.matrix.sesquilinear_form
linear_algebra.matrix.special_linear_group
linear_algebra.matrix.symmetric
linear_algebra.matrix.to_lin
linear_algebra.matrix.to_linear_equiv
linear_algebra.matrix.trace
linear_algebra.multilinear.basic
linear_algebra.multilinear.basis
linear_algebra.multilinear.tensor_product
linear_algebra.pi
linear_algebra.prod
linear_algebra.projection
linear_algebra.quadratic_form.basic
linear_algebra.quadratic_form.isometry
linear_algebra.quadratic_form.prod
linear_algebra.quotient
linear_algebra.ray
linear_algebra.sesquilinear_form
linear_algebra.span
linear_algebra.std_basis
linear_algebra.tensor_algebra.basic
linear_algebra.tensor_product
linear_algebra.tensor_product_basis
logic.basic
logic.denumerable
logic.embedding.basic
logic.embedding.set
logic.encodable.basic
logic.encodable.lattice
logic.equiv.basic
logic.equiv.defs
logic.equiv.fin
logic.equiv.fintype
logic.equiv.functor
logic.equiv.list
logic.equiv.local_equiv
logic.equiv.nat
logic.equiv.option
logic.equiv.set
logic.function.basic
logic.function.conjugate
logic.function.iterate
logic.is_empty
logic.lemmas
logic.nonempty
logic.nontrivial
logic.pairwise
logic.relation
logic.relator
logic.small.basic
logic.unique
meta.expr
meta.expr_lens
meta.rb_map
meta.univs
order.antichain
order.antisymmetrization
order.atoms
order.basic
order.boolean_algebra
order.bounded
order.bounded_order
order.bounds.basic
order.bounds.order_iso
order.chain
order.closure
order.compactly_generated
order.compare
order.complete_boolean_algebra
order.complete_lattice
order.complete_lattice_intervals
order.conditionally_complete_lattice.basic
order.conditionally_complete_lattice.finset
order.conditionally_complete_lattice.group
order.copy
order.cover
order.directed
order.disjoint
order.filter.archimedean
order.filter.at_top_bot
order.filter.bases
order.filter.basic
order.filter.cofinite
order.filter.countable_Inter
order.filter.extr
order.filter.interval
order.filter.lift
order.filter.n_ary
order.filter.pi
order.filter.pointwise
order.filter.prod
order.filter.small_sets
order.filter.ultrafilter
order.fixed_points
order.galois_connection
order.heyting.basic
order.hom.basic
order.hom.bounded
order.hom.complete_lattice
order.hom.lattice
order.hom.order
order.hom.set
order.initial_seg
order.iterate
order.lattice
order.lattice_intervals
order.liminf_limsup
order.locally_finite
order.max
order.min_max
order.minimal
order.modular_lattice
order.monotone.basic
order.omega_complete_partial_order
order.order_iso_nat
order.partial_sups
order.prop_instances
order.rel_classes
order.rel_iso.basic
order.rel_iso.set
order.succ_pred.basic
order.succ_pred.limit
order.succ_pred.relation
order.sup_indep
order.symm_diff
order.synonym
order.upper_lower.basic
order.well_founded
order.well_founded_set
order.with_bot
order.zorn
order.zorn_atoms
ring_theory.adjoin.basic
ring_theory.algebra_tower
ring_theory.congruence
ring_theory.coprime.basic
ring_theory.coprime.lemmas
ring_theory.euclidean_domain
ring_theory.finiteness
ring_theory.graded_algebra.basic
ring_theory.ideal.basic
ring_theory.ideal.operations
ring_theory.ideal.quotient
ring_theory.int.basic
ring_theory.localization.basic
ring_theory.localization.fraction_ring
ring_theory.localization.integer
ring_theory.multiplicity
ring_theory.mv_polynomial.basic
ring_theory.mv_polynomial.ideal
ring_theory.nilpotent
ring_theory.noetherian
ring_theory.non_zero_divisors
ring_theory.polynomial.basic
ring_theory.polynomial.content
ring_theory.principal_ideal_domain
ring_theory.subring.basic
ring_theory.subsemiring.basic
ring_theory.tensor_product
ring_theory.unique_factorization_domain
ring_theory.valuation.basic
set_theory.cardinal.basic
set_theory.cardinal.cofinality
set_theory.cardinal.finite
set_theory.cardinal.ordinal
set_theory.cardinal.schroeder_bernstein
set_theory.ordinal.arithmetic
set_theory.ordinal.basic
set_theory.ordinal.exponential
set_theory.ordinal.fixed_point
set_theory.ordinal.principal
tactic.abel
tactic.algebra
tactic.alias
tactic.apply
tactic.apply_fun
tactic.assert_exists
tactic.auto_cases
tactic.binder_matching
tactic.by_contra
tactic.cache
tactic.cancel_denoms
tactic.chain
tactic.choose
tactic.clear
tactic.compute_degree
tactic.congr
tactic.congrm
tactic.converter.apply_congr
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.expand_exists
tactic.explode
tactic.ext
tactic.field_simp
tactic.fin_cases
tactic.find
tactic.finish
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.linear_combination
tactic.lint.basic
tactic.lint.default
tactic.lint.frontend
tactic.lint.misc
tactic.lint.simp
tactic.lint.type_classes
tactic.localized
tactic.mk_iff_of_inductive_prop
tactic.mk_simp_attribute
tactic.monotonicity.basic
tactic.monotonicity.interactive
tactic.noncomm_ring
tactic.nontriviality
tactic.norm_cast
tactic.norm_fin
tactic.norm_num
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.polyrith
tactic.positivity
tactic.pretty_cases
tactic.print_sorry
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.ring
tactic.ring_exp
tactic.scc
tactic.show_term
tactic.simp_command
tactic.simp_result
tactic.simp_rw
tactic.simpa
tactic.simps
tactic.slice
tactic.solve_by_elim
tactic.split_ifs
tactic.squeeze
tactic.subtype_instance
tactic.suggest
tactic.tauto
tactic.tfae
tactic.tidy
tactic.to_additive
tactic.transform_decl
tactic.transport
tactic.trunc_cases
tactic.unfold_cases
tactic.unify_equations
tactic.where
tactic.with_local_reducibility
tactic.wlog
tactic.zify
topology.algebra.affine
topology.algebra.algebra
topology.algebra.const_mul_action
topology.algebra.constructions
topology.algebra.field
topology.algebra.filter_basis
topology.algebra.group.basic
topology.algebra.group_completion
topology.algebra.group_with_zero
topology.algebra.infinite_sum.basic
topology.algebra.infinite_sum.module
topology.algebra.infinite_sum.order
topology.algebra.infinite_sum.real
topology.algebra.infinite_sum.ring
topology.algebra.module.basic
topology.algebra.module.multilinear
topology.algebra.module.star
topology.algebra.module.strong_topology
topology.algebra.monoid
topology.algebra.mul_action
topology.algebra.order.archimedean
topology.algebra.order.compact
topology.algebra.order.field
topology.algebra.order.group
topology.algebra.order.intermediate_value
topology.algebra.order.left_right
topology.algebra.order.liminf_limsup
topology.algebra.order.monotone_continuity
topology.algebra.order.monotone_convergence
topology.algebra.order.proj_Icc
topology.algebra.ring.basic
topology.algebra.ring.ideal
topology.algebra.star
topology.algebra.star_subalgebra
topology.algebra.uniform_convergence
topology.algebra.uniform_group
topology.algebra.uniform_mul_action
topology.algebra.uniform_ring
topology.bases
topology.basic
topology.bornology.basic
topology.bornology.constructions
topology.bornology.hom
topology.compact_open
topology.connected
topology.constructions
topology.continuous_function.basic
topology.continuous_on
topology.dense_embedding
topology.homeomorph
topology.inseparable
topology.instances.ennreal
topology.instances.int
topology.instances.nat
topology.instances.nnreal
topology.instances.rat
topology.instances.real
topology.instances.real_vector_space
topology.local_extr
topology.local_homeomorph
topology.locally_finite
topology.maps
topology.metric_space.algebra
topology.metric_space.antilipschitz
topology.metric_space.basic
topology.metric_space.completion
topology.metric_space.emetric_space
topology.metric_space.hausdorff_distance
topology.metric_space.isometric_smul
topology.metric_space.isometry
topology.metric_space.lipschitz
topology.nhds_set
topology.order
topology.order.basic
topology.path_connected
topology.separation
topology.sequences
topology.sets.opens
topology.subset_properties
topology.support
topology.tactic
topology.uniform_space.abstract_completion
topology.uniform_space.basic
topology.uniform_space.cauchy
topology.uniform_space.compact
topology.uniform_space.complete_separated
topology.uniform_space.completion
topology.uniform_space.equicontinuity
topology.uniform_space.equiv
topology.uniform_space.pi
topology.uniform_space.separation
topology.uniform_space.uniform_convergence
topology.uniform_space.uniform_convergence_topology
topology.uniform_space.uniform_embedding
topology.unit_interval
debugger
.
attr
source
meta
def
debugger
.
attr
:
(
user_attribute
unit
)
General documentation
index
foundational types
tactics
commands
hole commands
attributes
notes
references
Additional documentation
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
feature_search
float
format
fun_info
has_reflect
hole_command
injection_tactic
instance_cache
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
lean-ga
examples
recursors
for_mathlib
algebra
algebra
opposite
algebra_operations
center_submonoid
filtration
monoid_algebra
ring_quot
linear_algebra
bilinear_form
basic
tensor_product
quadratic_form
isometric_map
prod
tensor_product
inner_product_space
opposite
tensor_product
ring_theory
tensor_product
geometric_algebra
from_mathlib
concrete
cga
default
pga
basic
category_theory
complexification
conjugation
contract
default
even_odd
even_odd_equiv
fold
mathoverflow
versors
zmod_grading
nursery
chisolm
graded
instances
translations
hol_light
ida
ida_derived
laurents
mathlib
algebra
algebra
subalgebra
basic
tower
basic
bilinear
equiv
hom
operations
pi
prod
restrict_scalars
tower
big_operators
multiset
basic
lemmas
associated
basic
fin
finprod
finsupp
intervals
nat_antidiagonal
option
order
pi
ring
ring_equiv
category
Algebra
basic
Group
basic
preadditive
Module
basic
Mon
basic
Ring
basic
char_p
algebra
basic
invertible
pi
quotient
two
char_zero
defs
infinite
lemmas
direct_sum
algebra
basic
decomposition
finsupp
internal
module
ring
divisibility
basic
units
euclidean_domain
basic
defs
instances
field
basic
defs
opposite
free_monoid
basic
gcd_monoid
basic
finset
multiset
group
with_one
defs
basic
commutator
commute
conj
defs
ext
inj_surj
opposite
order_synonym
pi
prod
semiconj
type_tags
ulift
units
group_power
basic
lemmas
order
ring
group_ring_action
basic
subobjects
group_with_zero
units
basic
lemmas
basic
commute
defs
divisibility
inj_surj
power
semiconj
hom
equiv
units
basic
group_with_zero
basic
aut
commute
embedding
group
group_action
group_instances
iterate
non_unital_alg
ring
units
module
submodule
basic
bilinear
lattice
pointwise
algebra
basic
big_operators
equiv
hom
linear_map
opposites
pi
prod
ulift
monoid_algebra
basic
division
ideal
support
order
field
canonical
basic
defs
basic
defs
inj_surj
power
group
abs
bounds
defs
inj_surj
instances
min_max
order_iso
type_tags
units
hom
basic
monoid
cancel
basic
defs
canonical
defs
with_zero
basic
defs
basic
defs
lemmas
min_max
nat_cast
order_dual
prod
type_tags
units
with_top
nonneg
field
floor
ring
positive
ring
ring
abs
canonical
char_zero
defs
inj_surj
lemmas
with_top
sub
canonical
defs
with_top
absolute_value
archimedean
floor
invertible
kleene
module
pi
smul
with_zero
zero_le_one
polynomial
big_operators
regular
basic
smul
ring
aut
basic
commute
comp_typeclasses
defs
divisibility
equiv
fin
idempotents
inj_surj
opposite
pi
prod
regular
semiconj
ulift
units
star
basic
big_operators
module
order
pi
pointwise
prod
self_adjoint
star_alg_hom
subalgebra
unitary
abs
add_torsor
associated
bounds
covariant_and_contravariant
dual_number
free_algebra
geom_sum
graded_monoid
indicator_function
invertible
ne_zero
opposites
parity
periodic
punit_instances
quaternion
quaternion_basis
quotient
ring_quot
smul_with_zero
support
triv_sq_zero_ext
analysis
asymptotics
asymptotics
complex
basic
convex
basic
combination
function
hull
jensen
normed
segment
star
strict
strict_convex_space
topology
uniform
inner_product_space
basic
locally_convex
balanced_core_hull
basic
bounded
normed
field
basic
group
add_torsor
basic
completion
hom
infinite_sum
pointwise
seminorm
order
basic
mul_action
normed_space
star
basic
add_torsor
affine_isometry
basic
bounded_linear_maps
completion
continuous_linear_map
linear_isometry
multilinear
operator_norm
pointwise
ray
units
specific_limits
basic
normed
seminorm
category_theory
adjunction
basic
bicategory
basic
strict
category
Cat
basic
preorder
ulift
concrete_category
basic
bundled
bundled_hom
reflects_isomorphisms
functor
basic
category
const
currying
epi_mono
fully_faithful
hom
reflects_isomorphisms
lifting_properties
adjunction
basic
limits
constructions
epi_mono
preserves
shapes
binary_products
biproducts
products
pullbacks
terminal
zero
basic
finite
shapes
binary_products
biproducts
equalizers
finite_limits
finite_products
images
kernels
products
pullbacks
strong_epi
terminal
wide_pullbacks
zero_morphisms
zero_objects
cones
exact_functor
has_limits
is_limit
linear
basic
pi
basic
preadditive
additive_functor
basic
biproducts
functor_category
products
basic
bifunctor
arrow
balanced
comm_sq
comma
conj
discrete_category
elementwise
endomorphism
epi_mono
eq_to_hom
equivalence
essential_image
essentially_small
fin_category
full_subcategory
groupoid
isomorphism
isomorphism_classes
natural_isomorphism
natural_transformation
opposites
over
pempty
punit
skeletal
structured_arrow
thin
types
whiskering
yoneda
combinatorics
quiver
basic
connected_component
path
push
subquiver
symmetric
composition
partition
control
equiv_functor
instances
monad
basic
traversable
basic
derive
equiv
instances
lemmas
applicative
basic
bifunctor
equiv_functor
functor
data
array
lemmas
bool
basic
set
buffer
parser
basic
numeral
basic
complex
basic
exponential
module
countable
basic
defs
dfinsupp
basic
dlist
basic
enat
basic
lattice
fin
tuple
basic
basic
interval
vec_notation
finite
basic
card
defs
set
finset
basic
card
fin
fold
image
lattice
locally_finite
n_ary
nat_antidiagonal
noncomm_prod
option
order
pairwise
pi
pointwise
powerset
preimage
prod
sigma
sort
sum
finsupp
antidiagonal
basic
defs
fin
indicator
multiset
order
to_dfinsupp
fintype
basic
big_operators
card
fin
lattice
list
option
perm
pi
powerset
prod
sigma
sort
sum
units
vector
fun_like
basic
embedding
equiv
int
cast
basic
defs
field
lemmas
prod
dvd
basic
order
basic
lemmas
units
basic
bitwise
char_zero
div
gcd
interval
least_greatest
lemmas
modeq
parity
units
is_R_or_C
basic
list
big_operators
basic
lemmas
basic
chain
count
cycle
dedup
defs
duplicate
fin_range
forall2
func
indexes
infix
join
lattice
lex
min_max
nat_antidiagonal
nodup
nodup_equiv_fin
of_fn
pairwise
palindrome
perm
permutation
prime
prod_sigma
range
rotate
sort
sublists
tfae
zip
matrix
basic
basis
block
invertible
notation
pequiv
multiset
antidiagonal
basic
bind
dedup
finset_ops
fold
lattice
nat_antidiagonal
nodup
pi
powerset
range
sort
sum
mv_polynomial
basic
comm_ring
division
equiv
rename
variables
nat
cast
basic
defs
field
prod
choose
basic
sum
factorial
basic
gcd
basic
order
basic
lemmas
basic
bits
bitwise
digits
factors
interval
lattice
log
modeq
multiplicity
pairing
parity
part_enat
pow
prime
set
size
sqrt
succ_pred
units
with_bot
num
basic
option
basic
defs
n_ary
pi
algebra
lex
pnat
basic
defs
interval
polynomial
degree
definitions
lemmas
trailing_degree
algebra_map
basic
cancel_leads
coeff
derivative
div
erase_lead
eval
field_division
induction
inductions
monic
monomial
reverse
ring_division
prod
basic
lex
pprod
rat
basic
big_operators
cast
defs
floor
init
lemmas
meta_defs
order
rbmap
basic
rbtree
default_lt
init
real
basic
cau_seq
cau_seq_completion
ennreal
nnreal
pointwise
sqrt
set
intervals
basic
disjoint
group
infinite
instances
monoid
ord_connected
order_iso
pi
proj_Icc
unordered_interval
pairwise
basic
lattice
pointwise
basic
big_operators
finite
interval
list_of_fn
smul
Union_lift
accumulate
basic
bool_indicator
countable
finite
function
functor
image
lattice
list
n_ary
prod
semiring
sigma
set_like
basic
setoid
basic
sigma
basic
lex
string
basic
defs
sum
basic
order
sym
basic
vector
basic
zmod
basic
defs
bracket
char
json
mllist
opposite
part
pequiv
quot
sign
subtype
tree
ulift
dynamics
fixed_points
basic
periodic_pts
field_theory
finiteness
mv_polynomial
subfield
tower
group_theory
group_action
sub_mul_action
pointwise
basic
big_operators
conj_act
defs
group
opposite
pi
prod
quotient
sub_mul_action
units
perm
cycle
basic
type
basic
fin
list
option
sign
subgroup
support
subgroup
actions
basic
finite
mul_opposite
pointwise
zpowers
submonoid
basic
center
centralizer
membership
operations
pointwise
subsemigroup
basic
center
centralizer
operations
archimedean
commutator
congruence
coset
finiteness
index
monoid_localization
order_of_element
quotient_group
linear_algebra
affine_space
affine_equiv
affine_map
affine_subspace
basic
basis
combination
independent
midpoint
midpoint_zero
restrict
basis
bilinear
bilinear_form
tensor_product
clifford_algebra
basic
conjugation
contraction
equivs
even
even_equiv
fold
grading
star
direct_sum
finsupp
tensor_product
exterior_algebra
basic
free_module
finite
basic
matrix
rank
basic
rank
matrix
adjugate
basis
bilinear_form
determinant
general_linear_group
mv_polynomial
nondegenerate
nonsingular_inverse
polynomial
reindex
sesquilinear_form
special_linear_group
symmetric
to_lin
to_linear_equiv
trace
multilinear
basic
basis
tensor_product
quadratic_form
basic
isometry
prod
tensor_algebra
basic
alternating
basic
basis
bilinear_form
bilinear_map
dfinsupp
dimension
dual
finite_dimensional
finrank
finsupp
finsupp_vector_space
general_linear_group
invariant_basis_number
isomorphisms
linear_independent
linear_pmap
pi
prod
projection
quotient
ray
sesquilinear_form
span
std_basis
tensor_product
tensor_product_basis
logic
embedding
basic
set
encodable
basic
lattice
equiv
basic
defs
fin
fintype
functor
list
local_equiv
nat
option
set
function
basic
conjugate
iterate
small
basic
basic
denumerable
is_empty
lemmas
nonempty
nontrivial
pairwise
relation
relator
unique
meta
expr
expr_lens
rb_map
univs
order
bounds
basic
order_iso
conditionally_complete_lattice
basic
finset
group
filter
archimedean
at_top_bot
bases
basic
cofinite
countable_Inter
extr
interval
lift
n_ary
pi
pointwise
prod
small_sets
ultrafilter
heyting
basic
hom
basic
bounded
complete_lattice
lattice
order
set
monotone
basic
rel_iso
basic
set
succ_pred
basic
limit
relation
upper_lower
basic
antichain
antisymmetrization
atoms
basic
boolean_algebra
bounded
bounded_order
chain
closure
compactly_generated
compare
complete_boolean_algebra
complete_lattice
complete_lattice_intervals
copy
cover
directed
disjoint
fixed_points
galois_connection
initial_seg
iterate
lattice
lattice_intervals
liminf_limsup
locally_finite
max
min_max
minimal
modular_lattice
omega_complete_partial_order
order_iso_nat
partial_sups
prop_instances
rel_classes
sup_indep
symm_diff
synonym
well_founded
well_founded_set
with_bot
zorn
zorn_atoms
ring_theory
adjoin
basic
coprime
basic
lemmas
graded_algebra
basic
ideal
basic
operations
quotient
int
basic
localization
basic
fraction_ring
integer
mv_polynomial
basic
ideal
polynomial
basic
content
subring
basic
subsemiring
basic
valuation
basic
algebra_tower
congruence
euclidean_domain
finiteness
multiplicity
nilpotent
noetherian
non_zero_divisors
principal_ideal_domain
tensor_product
unique_factorization_domain
set_theory
cardinal
basic
cofinality
finite
ordinal
schroeder_bernstein
ordinal
arithmetic
basic
exponential
fixed_point
principal
tactic
converter
apply_congr
interactive
old_conv
linarith
datatypes
elimination
frontend
lemmas
parsing
preprocessing
verification
lint
basic
default
frontend
misc
simp
type_classes
monotonicity
basic
interactive
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
abel
algebra
alias
apply
apply_fun
assert_exists
auto_cases
binder_matching
by_contra
cache
cancel_denoms
chain
choose
clear
compute_degree
congr
congrm
core
dec_trivial
delta_instance
dependencies
derive_fintype
derive_inhabited
doc_commands
elementwise
elide
equiv_rw
expand_exists
explode
ext
field_simp
fin_cases
find
finish
fresh_names
generalize_proofs
generalizes
group
has_variable_names
hint
induction
interactive
interactive_expr
interval_cases
itauto
lean_core_docs
lift
linear_combination
localized
mk_iff_of_inductive_prop
mk_simp_attribute
noncomm_ring
nontriviality
norm_cast
norm_fin
norm_num
obviously
pi_instances
polyrith
positivity
pretty_cases
print_sorry
project_dir
protected
push_neg
rcases
reassoc_axiom
rename_var
replacer
reserved_notation
restate_axiom
rewrite
ring
ring_exp
scc
show_term
simp_command
simp_result
simp_rw
simpa
simps
slice
solve_by_elim
split_ifs
squeeze
subtype_instance
suggest
tauto
tfae
tidy
to_additive
transform_decl
transport
trunc_cases
unfold_cases
unify_equations
where
with_local_reducibility
wlog
zify
topology
algebra
group
basic
infinite_sum
basic
module
order
real
ring
module
basic
multilinear
star
strong_topology
order
archimedean
compact
field
group
intermediate_value
left_right
liminf_limsup
monotone_continuity
monotone_convergence
proj_Icc
ring
basic
ideal
affine
algebra
const_mul_action
constructions
field
filter_basis
group_completion
group_with_zero
monoid
mul_action
star
star_subalgebra
uniform_convergence
uniform_group
uniform_mul_action
uniform_ring
bornology
basic
constructions
hom
continuous_function
basic
instances
ennreal
int
nat
nnreal
rat
real
real_vector_space
metric_space
algebra
antilipschitz
basic
completion
emetric_space
hausdorff_distance
isometric_smul
isometry
lipschitz
order
basic
sets
opens
uniform_space
abstract_completion
basic
cauchy
compact
complete_separated
completion
equicontinuity
equiv
pi
separation
uniform_convergence
uniform_convergence_topology
uniform_embedding
bases
basic
compact_open
connected
constructions
continuous_on
dense_embedding
homeomorph
inseparable
local_extr
local_homeomorph
locally_finite
maps
nhds_set
order
path_connected
separation
sequences
subset_properties
support
tactic
unit_interval
Color scheme
dark
system
light