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.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
algebra.abs
algebra.add_torsor
algebra.algebra.basic
algebra.algebra.bilinear
algebra.algebra.operations
algebra.algebra.restrict_scalars
algebra.algebra.spectrum
algebra.algebra.subalgebra.basic
algebra.algebra.subalgebra.pointwise
algebra.algebra.tower
algebra.algebra.unitization
algebra.algebraic_card
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
algebra.big_operators.nat_antidiagonal
algebra.big_operators.norm_num
algebra.big_operators.option
algebra.big_operators.order
algebra.big_operators.part_enat
algebra.big_operators.pi
algebra.big_operators.ring
algebra.bounds
algebra.category.Algebra.basic
algebra.category.Algebra.limits
algebra.category.BoolRing
algebra.category.FinVect
algebra.category.FinVect.limits
algebra.category.Group.Z_Module_equivalence
algebra.category.Group.abelian
algebra.category.Group.adjunctions
algebra.category.Group.basic
algebra.category.Group.biproducts
algebra.category.Group.colimits
algebra.category.Group.epi_mono
algebra.category.Group.equivalence_Group_AddGroup
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.GroupWithZero
algebra.category.Module.abelian
algebra.category.Module.adjunctions
algebra.category.Module.basic
algebra.category.Module.biproducts
algebra.category.Module.change_of_rings
algebra.category.Module.colimits
algebra.category.Module.epi_mono
algebra.category.Module.filtered_colimits
algebra.category.Module.images
algebra.category.Module.kernels
algebra.category.Module.limits
algebra.category.Module.monoidal
algebra.category.Module.products
algebra.category.Module.projective
algebra.category.Module.simple
algebra.category.Module.subobject
algebra.category.Module.tannaka
algebra.category.Mon.adjunctions
algebra.category.Mon.basic
algebra.category.Mon.colimits
algebra.category.Mon.filtered_colimits
algebra.category.Mon.limits
algebra.category.Ring.adjunctions
algebra.category.Ring.basic
algebra.category.Ring.colimits
algebra.category.Ring.constructions
algebra.category.Ring.filtered_colimits
algebra.category.Ring.instances
algebra.category.Ring.limits
algebra.category.Semigroup.basic
algebra.char_p.algebra
algebra.char_p.basic
algebra.char_p.char_and_card
algebra.char_p.exp_char
algebra.char_p.invertible
algebra.char_p.local_ring
algebra.char_p.pi
algebra.char_p.quotient
algebra.char_p.subring
algebra.char_p.two
algebra.char_zero
algebra.char_zero.defs
algebra.char_zero.quotient
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.cubic_discriminant
algebra.direct_limit
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
algebra.dual_number
algebra.euclidean_domain
algebra.field.basic
algebra.field.opposite
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.integrally_closed
algebra.gcd_monoid.multiset
algebra.gcd_monoid.nat
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.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.with_one
algebra.group_power.basic
algebra.group_power.identities
algebra.group_power.lemmas
algebra.group_power.order
algebra.group_power.ring
algebra.group_ring_action
algebra.group_with_zero.basic
algebra.group_with_zero.defs
algebra.group_with_zero.power
algebra.hierarchy_design
algebra.hom.aut
algebra.hom.centroid
algebra.hom.equiv
algebra.hom.freiman
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.homology.Module
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.short_exact.abelian
algebra.homology.short_exact.preadditive
algebra.homology.single
algebra.indicator_function
algebra.invertible
algebra.is_prime_pow
algebra.jordan.basic
algebra.lie.abelian
algebra.lie.base_change
algebra.lie.basic
algebra.lie.cartan_matrix
algebra.lie.cartan_subalgebra
algebra.lie.centralizer
algebra.lie.character
algebra.lie.classical
algebra.lie.direct_sum
algebra.lie.engel
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.algebra
algebra.module.basic
algebra.module.bimodule
algebra.module.dedekind_domain
algebra.module.default
algebra.module.equiv
algebra.module.hom
algebra.module.injective
algebra.module.linear_map
algebra.module.localized_module
algebra.module.opposites
algebra.module.pi
algebra.module.pid
algebra.module.pointwise_pi
algebra.module.prod
algebra.module.projective
algebra.module.submodule.basic
algebra.module.submodule.bilinear
algebra.module.submodule.lattice
algebra.module.submodule.pointwise
algebra.module.torsion
algebra.module.ulift
algebra.monoid_algebra.basic
algebra.monoid_algebra.degree
algebra.monoid_algebra.grading
algebra.monoid_algebra.no_zero_divisors
algebra.monoid_algebra.support
algebra.monoid_algebra.to_direct_sum
algebra.ne_zero
algebra.opposites
algebra.order.absolute_value
algebra.order.algebra
algebra.order.archimedean
algebra.order.complete_field
algebra.order.euclidean_absolute_value
algebra.order.field
algebra.order.field_defs
algebra.order.floor
algebra.order.group
algebra.order.hom.basic
algebra.order.hom.monoid
algebra.order.hom.ring
algebra.order.invertible
algebra.order.lattice_group
algebra.order.module
algebra.order.monoid
algebra.order.monoid_lemmas
algebra.order.monoid_lemmas_zero_lt
algebra.order.nonneg
algebra.order.pi
algebra.order.pointwise
algebra.order.positive.field
algebra.order.positive.ring
algebra.order.rearrangement
algebra.order.ring
algebra.order.smul
algebra.order.sub
algebra.order.to_interval_mod
algebra.order.with_zero
algebra.parity
algebra.pempty_instances
algebra.periodic
algebra.polynomial.big_operators
algebra.polynomial.group_ring_action
algebra.punit_instances
algebra.quadratic_discriminant
algebra.quandle
algebra.quaternion
algebra.quaternion_basis
algebra.quotient
algebra.regular.basic
algebra.regular.pow
algebra.regular.smul
algebra.ring.aut
algebra.ring.basic
algebra.ring.boolean_ring
algebra.ring.comp_typeclasses
algebra.ring.default
algebra.ring.equiv
algebra.ring.idempotents
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.free
algebra.star.module
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.symmetrized
algebra.triv_sq_zero_ext
algebra.tropical.basic
algebra.tropical.big_operators
algebra.tropical.lattice
algebraic_geometry.AffineScheme
algebraic_geometry.EllipticCurve
algebraic_geometry.Gamma_Spec_adjunction
algebraic_geometry.Scheme
algebraic_geometry.Spec
algebraic_geometry.function_field
algebraic_geometry.gluing
algebraic_geometry.limits
algebraic_geometry.locally_ringed_space
algebraic_geometry.locally_ringed_space.has_colimits
algebraic_geometry.morphisms.basic
algebraic_geometry.morphisms.quasi_compact
algebraic_geometry.morphisms.ring_hom_properties
algebraic_geometry.open_immersion
algebraic_geometry.presheafed_space
algebraic_geometry.presheafed_space.gluing
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.projective_spectrum.scheme
algebraic_geometry.projective_spectrum.structure_sheaf
algebraic_geometry.projective_spectrum.topology
algebraic_geometry.properties
algebraic_geometry.pullbacks
algebraic_geometry.ringed_space
algebraic_geometry.sheafed_space
algebraic_geometry.stalks
algebraic_geometry.structure_sheaf
algebraic_topology.Moore_complex
algebraic_topology.alternating_face_map_complex
algebraic_topology.cech_nerve
algebraic_topology.dold_kan.faces
algebraic_topology.dold_kan.functor_n
algebraic_topology.dold_kan.homotopies
algebraic_topology.dold_kan.homotopy_equivalence
algebraic_topology.dold_kan.normalized
algebraic_topology.dold_kan.notations
algebraic_topology.dold_kan.p_infty
algebraic_topology.dold_kan.projections
algebraic_topology.fundamental_groupoid.basic
algebraic_topology.fundamental_groupoid.fundamental_group
algebraic_topology.fundamental_groupoid.induced_maps
algebraic_topology.fundamental_groupoid.product
algebraic_topology.fundamental_groupoid.punit
algebraic_topology.fundamental_groupoid.simply_connected
algebraic_topology.nerve
algebraic_topology.simplex_category
algebraic_topology.simplicial_object
algebraic_topology.simplicial_set
algebraic_topology.split_simplicial_object
algebraic_topology.topological_simplex
analysis.ODE.gronwall
analysis.ODE.picard_lindelof
analysis.analytic.basic
analysis.analytic.composition
analysis.analytic.inverse
analysis.analytic.isolated_zeros
analysis.analytic.linear
analysis.analytic.radius_liminf
analysis.asymptotics.asymptotic_equivalent
analysis.asymptotics.asymptotics
analysis.asymptotics.specific_asymptotics
analysis.asymptotics.superpolynomial_decay
analysis.asymptotics.theta
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.cont_diff
analysis.calculus.darboux
analysis.calculus.deriv
analysis.calculus.diff_on_int_cont
analysis.calculus.dslope
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.taylor
analysis.calculus.uniform_limits_deriv
analysis.complex.abs_max
analysis.complex.arg
analysis.complex.basic
analysis.complex.cauchy_integral
analysis.complex.circle
analysis.complex.conformal
analysis.complex.isometry
analysis.complex.liouville
analysis.complex.phragmen_lindelof
analysis.complex.polynomial
analysis.complex.re_im_topology
analysis.complex.real_deriv
analysis.complex.removable_singularity
analysis.complex.roots_of_unity
analysis.complex.schwarz
analysis.complex.upper_half_plane.basic
analysis.complex.upper_half_plane.functions_bounded_at_infty
analysis.complex.upper_half_plane.metric
analysis.complex.upper_half_plane.topology
analysis.convex.basic
analysis.convex.caratheodory
analysis.convex.combination
analysis.convex.complex
analysis.convex.cone.basic
analysis.convex.contractible
analysis.convex.exposed
analysis.convex.extrema
analysis.convex.extreme
analysis.convex.function
analysis.convex.gauge
analysis.convex.hull
analysis.convex.independent
analysis.convex.integral
analysis.convex.jensen
analysis.convex.join
analysis.convex.krein_milman
analysis.convex.measure
analysis.convex.partition_of_unity
analysis.convex.quasiconvex
analysis.convex.segment
analysis.convex.simplicial_complex.basic
analysis.convex.slope
analysis.convex.specific_functions
analysis.convex.star
analysis.convex.stone_separation
analysis.convex.strict
analysis.convex.strict_convex_space
analysis.convex.topology
analysis.convex.uniform
analysis.convolution
analysis.fourier
analysis.hofer
analysis.inner_product_space.adjoint
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.gram_schmidt_ortho
analysis.inner_product_space.l2_space
analysis.inner_product_space.lax_milgram
analysis.inner_product_space.orientation
analysis.inner_product_space.pi_L2
analysis.inner_product_space.positive
analysis.inner_product_space.projection
analysis.inner_product_space.rayleigh
analysis.inner_product_space.spectrum
analysis.inner_product_space.symmetric
analysis.locally_convex.balanced_core_hull
analysis.locally_convex.basic
analysis.locally_convex.bounded
analysis.locally_convex.polar
analysis.locally_convex.weak_dual
analysis.locally_convex.with_seminorms
analysis.matrix
analysis.mean_inequalities
analysis.mean_inequalities_pow
analysis.normed.field.basic
analysis.normed.field.unit_ball
analysis.normed.group.SemiNormedGroup
analysis.normed.group.SemiNormedGroup.completion
analysis.normed.group.SemiNormedGroup.kernels
analysis.normed.group.add_torsor
analysis.normed.group.ball_sphere
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.pointwise
analysis.normed.group.quotient
analysis.normed.group.seminorm
analysis.normed.ring.seminorm
analysis.normed_space.M_structure
analysis.normed_space.add_torsor
analysis.normed_space.add_torsor_bases
analysis.normed_space.affine_isometry
analysis.normed_space.algebra
analysis.normed_space.ball_action
analysis.normed_space.banach
analysis.normed_space.banach_steinhaus
analysis.normed_space.basic
analysis.normed_space.bounded_linear_maps
analysis.normed_space.compact_operator
analysis.normed_space.complemented
analysis.normed_space.completion
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.extr
analysis.normed_space.finite_dimension
analysis.normed_space.hahn_banach.extension
analysis.normed_space.hahn_banach.separation
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.lp_space
analysis.normed_space.matrix_exponential
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.pointwise
analysis.normed_space.ray
analysis.normed_space.riesz_lemma
analysis.normed_space.spectrum
analysis.normed_space.star.basic
analysis.normed_space.star.complex
analysis.normed_space.star.exponential
analysis.normed_space.star.gelfand_duality
analysis.normed_space.star.matrix
analysis.normed_space.star.spectrum
analysis.normed_space.units
analysis.normed_space.weak_dual
analysis.p_series
analysis.quaternion
analysis.schwartz_space
analysis.seminorm
analysis.special_functions.arsinh
analysis.special_functions.bernstein
analysis.special_functions.compare_exp
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.gamma
analysis.special_functions.gaussian
analysis.special_functions.integrals
analysis.special_functions.log.base
analysis.special_functions.log.basic
analysis.special_functions.log.deriv
analysis.special_functions.log.monotone
analysis.special_functions.non_integrable
analysis.special_functions.polar_coord
analysis.special_functions.polynomials
analysis.special_functions.pow
analysis.special_functions.pow_deriv
analysis.special_functions.sqrt
analysis.special_functions.stirling
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.bounds
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.basic
analysis.specific_limits.floor_pow
analysis.specific_limits.normed
analysis.subadditive
analysis.sum_integral_comparisons
analysis.von_neumann_algebra.basic
category_theory.Fintype
category_theory.abelian.basic
category_theory.abelian.diagram_lemmas.four
category_theory.abelian.exact
category_theory.abelian.ext
category_theory.abelian.functor_category
category_theory.abelian.generator
category_theory.abelian.homology
category_theory.abelian.images
category_theory.abelian.injective_resolution
category_theory.abelian.left_derived
category_theory.abelian.non_preadditive
category_theory.abelian.opposite
category_theory.abelian.projective
category_theory.abelian.pseudoelements
category_theory.abelian.right_derived
category_theory.abelian.subobject
category_theory.abelian.transfer
category_theory.action
category_theory.additive.basic
category_theory.adjunction.adjoint_functor_theorems
category_theory.adjunction.basic
category_theory.adjunction.comma
category_theory.adjunction.evaluation
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.balanced
category_theory.bicategory.End
category_theory.bicategory.basic
category_theory.bicategory.coherence
category_theory.bicategory.coherence_tactic
category_theory.bicategory.free
category_theory.bicategory.functor
category_theory.bicategory.functor_bicategory
category_theory.bicategory.locally_discrete
category_theory.bicategory.natural_transformation
category_theory.bicategory.single_obj
category_theory.bicategory.strict
category_theory.category.Bipointed
category_theory.category.Cat
category_theory.category.Cat.limit
category_theory.category.Groupoid
category_theory.category.Kleisli
category_theory.category.PartialFun
category_theory.category.Pointed
category_theory.category.Quiv
category_theory.category.Rel
category_theory.category.Twop
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.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.elementwise
category_theory.concrete_category.reflects_isomorphisms
category_theory.concrete_category.unbundled_hom
category_theory.conj
category_theory.connected_components
category_theory.core
category_theory.differential_object
category_theory.discrete_category
category_theory.elements
category_theory.elementwise
category_theory.endofunctor.algebra
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.functor.basic
category_theory.functor.category
category_theory.functor.const
category_theory.functor.currying
category_theory.functor.epi_mono
category_theory.functor.flat
category_theory.functor.fully_faithful
category_theory.functor.functorial
category_theory.functor.hom
category_theory.functor.inv_isos
category_theory.functor.left_derived
category_theory.functor.reflects_isomorphisms
category_theory.generator
category_theory.glue_data
category_theory.graded_object
category_theory.grothendieck
category_theory.groupoid
category_theory.idempotents.basic
category_theory.idempotents.biproducts
category_theory.idempotents.functor_categories
category_theory.idempotents.functor_extension
category_theory.idempotents.karoubi
category_theory.idempotents.karoubi_karoubi
category_theory.idempotents.simplicial_object
category_theory.is_connected
category_theory.isomorphism
category_theory.isomorphism_classes
category_theory.lifting_properties.adjunction
category_theory.lifting_properties.basic
category_theory.limits.bicones
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.essentially_small
category_theory.limits.exact_functor
category_theory.limits.filtered_colimit_commutes_finite_limit
category_theory.limits.final
category_theory.limits.fubini
category_theory.limits.full_subcategory
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.finite
category_theory.limits.preserves.functor_category
category_theory.limits.preserves.limits
category_theory.limits.preserves.opposites
category_theory.limits.preserves.shapes.binary_products
category_theory.limits.preserves.shapes.biproducts
category_theory.limits.preserves.shapes.equalizers
category_theory.limits.preserves.shapes.images
category_theory.limits.preserves.shapes.kernels
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.presheaf
category_theory.limits.shapes.binary_products
category_theory.limits.shapes.biproducts
category_theory.limits.shapes.comm_sq
category_theory.limits.shapes.concrete_category
category_theory.limits.shapes.diagonal
category_theory.limits.shapes.disjoint_coproduct
category_theory.limits.shapes.equalizers
category_theory.limits.shapes.equivalence
category_theory.limits.shapes.finite_limits
category_theory.limits.shapes.finite_products
category_theory.limits.shapes.functor_category
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.basic
category_theory.limits.shapes.normal_mono.equalizers
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_morphisms
category_theory.limits.shapes.zero_objects
category_theory.limits.small_complete
category_theory.limits.types
category_theory.limits.unit
category_theory.limits.yoneda
category_theory.linear.default
category_theory.linear.functor_category
category_theory.linear.linear_functor
category_theory.linear.yoneda
category_theory.localization.construction
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.coherence
category_theory.monoidal.coherence_lemmas
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.linear
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.basic
category_theory.monoidal.rigid.functor_category
category_theory.monoidal.rigid.of_equivalence
category_theory.monoidal.skeleton
category_theory.monoidal.subcategory
category_theory.monoidal.tor
category_theory.monoidal.transport
category_theory.monoidal.types
category_theory.morphism_property
category_theory.natural_isomorphism
category_theory.natural_transformation
category_theory.noetherian
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.eilenberg_moore
category_theory.preadditive.endo_functor
category_theory.preadditive.functor_category
category_theory.preadditive.generator
category_theory.preadditive.hom_orthogonal
category_theory.preadditive.injective
category_theory.preadditive.injective_resolution
category_theory.preadditive.left_exact
category_theory.preadditive.of_biproducts
category_theory.preadditive.opposite
category_theory.preadditive.projective
category_theory.preadditive.projective_resolution
category_theory.preadditive.schur
category_theory.preadditive.single_obj
category_theory.preadditive.yoneda
category_theory.products.associator
category_theory.products.basic
category_theory.products.bifunctor
category_theory.punit
category_theory.quotient
category_theory.shift
category_theory.sigma.basic
category_theory.simple
category_theory.single_obj
category_theory.sites.adjunction
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.left_exact
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.subsheaf
category_theory.sites.types
category_theory.sites.whiskering
category_theory.skeletal
category_theory.structured_arrow
category_theory.subobject.basic
category_theory.subobject.comma
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.additive.behrend
combinatorics.additive.pluennecke_ruzsa
combinatorics.additive.ruzsa_covering
combinatorics.additive.salem_spencer
combinatorics.catalan
combinatorics.colex
combinatorics.composition
combinatorics.configuration
combinatorics.derangements.basic
combinatorics.derangements.exponential
combinatorics.derangements.finite
combinatorics.double_counting
combinatorics.hales_jewett
combinatorics.hall.basic
combinatorics.hall.finite
combinatorics.hindman
combinatorics.partition
combinatorics.pigeonhole
combinatorics.quiver.arborescence
combinatorics.quiver.basic
combinatorics.quiver.connected_component
combinatorics.quiver.path
combinatorics.quiver.subquiver
combinatorics.set_family.compression.down
combinatorics.set_family.compression.uv
combinatorics.set_family.harris_kleitman
combinatorics.set_family.intersecting
combinatorics.set_family.kleitman
combinatorics.set_family.lym
combinatorics.set_family.shadow
combinatorics.simple_graph.adj_matrix
combinatorics.simple_graph.basic
combinatorics.simple_graph.clique
combinatorics.simple_graph.coloring
combinatorics.simple_graph.connectivity
combinatorics.simple_graph.degree_sum
combinatorics.simple_graph.density
combinatorics.simple_graph.hasse
combinatorics.simple_graph.inc_matrix
combinatorics.simple_graph.matching
combinatorics.simple_graph.metric
combinatorics.simple_graph.partition
combinatorics.simple_graph.prod
combinatorics.simple_graph.regularity.bound
combinatorics.simple_graph.regularity.energy
combinatorics.simple_graph.regularity.equitabilise
combinatorics.simple_graph.regularity.uniform
combinatorics.simple_graph.strongly_regular
combinatorics.simple_graph.subgraph
combinatorics.simple_graph.trails
combinatorics.simple_graph.triangle.basic
combinatorics.young_diagram
computability.DFA
computability.NFA
computability.ackermann
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.W.constructions
data.analysis.filter
data.analysis.topology
data.array.lemmas
data.bitvec.basic
data.bitvec.core
data.bool.all_any
data.bool.basic
data.bool.set
data.bracket
data.buffer.basic
data.buffer.parser.basic
data.buffer.parser.numeral
data.bundle
data.char
data.complex.basic
data.complex.cardinality
data.complex.determinant
data.complex.exponential
data.complex.exponential_bounds
data.complex.is_R_or_C
data.complex.module
data.countable.basic
data.countable.defs
data.countable.small
data.dfinsupp.basic
data.dfinsupp.interval
data.dfinsupp.order
data.dlist.basic
data.dlist.instances
data.erased
data.fin.basic
data.fin.fin2
data.fin.interval
data.fin.succ_pred
data.fin.tuple.basic
data.fin.tuple.monotone
data.fin.tuple.nat_antidiagonal
data.fin.tuple.sort
data.fin.vec_notation
data.fin_enum
data.finite.basic
data.finite.card
data.finite.defs
data.finite.set
data.finmap
data.finset.basic
data.finset.card
data.finset.fin
data.finset.finsupp
data.finset.fold
data.finset.functor
data.finset.interval
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.pi_induction
data.finset.pimage
data.finset.pointwise
data.finset.powerset
data.finset.preimage
data.finset.prod
data.finset.sigma
data.finset.slice
data.finset.sort
data.finset.sum
data.finset.sym
data.finsupp.antidiagonal
data.finsupp.basic
data.finsupp.big_operators
data.finsupp.default
data.finsupp.defs
data.finsupp.fin
data.finsupp.indicator
data.finsupp.interval
data.finsupp.lex
data.finsupp.multiset
data.finsupp.ne_locus
data.finsupp.order
data.finsupp.pointwise
data.finsupp.pwo
data.finsupp.to_dfinsupp
data.fintype.basic
data.fintype.card
data.fintype.card_embedding
data.fintype.fin
data.fintype.list
data.fintype.order
data.fintype.small
data.fintype.sort
data.fp.basic
data.fun_like.basic
data.fun_like.embedding
data.fun_like.equiv
data.hash_map
data.holor
data.int.absolute_value
data.int.basic
data.int.cast
data.int.cast.defs
data.int.cast_field
data.int.char_zero
data.int.gcd
data.int.interval
data.int.least_greatest
data.int.log
data.int.modeq
data.int.nat_prime
data.int.order
data.int.parity
data.int.range
data.int.sqrt
data.int.succ_pred
data.json
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.dedup
data.list.defs
data.list.destutter
data.list.duplicate
data.list.forall2
data.list.func
data.list.indexes
data.list.infix
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.prime
data.list.prod_sigma
data.list.range
data.list.rdrop
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.matrix.rank
data.mllist
data.multiset.antidiagonal
data.multiset.basic
data.multiset.bind
data.multiset.dedup
data.multiset.finset_ops
data.multiset.fintype
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.multiset.sum
data.mv_polynomial.basic
data.mv_polynomial.cardinal
data.mv_polynomial.comap
data.mv_polynomial.comm_ring
data.mv_polynomial.counit
data.mv_polynomial.derivation
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.bits
data.nat.bitwise
data.nat.cast
data.nat.cast.defs
data.nat.cast_field
data.nat.choose.basic
data.nat.choose.bounds
data.nat.choose.cast
data.nat.choose.central
data.nat.choose.dvd
data.nat.choose.factorization
data.nat.choose.multinomial
data.nat.choose.sum
data.nat.choose.vandermonde
data.nat.count
data.nat.digits
data.nat.dist
data.nat.enat
data.nat.factorial.basic
data.nat.factorial.big_operators
data.nat.factorial.cast
data.nat.factorization.basic
data.nat.factorization.prime_pow
data.nat.fib
data.nat.gcd
data.nat.interval
data.nat.lattice
data.nat.log
data.nat.modeq
data.nat.multiplicity
data.nat.nth
data.nat.pairing
data.nat.parity
data.nat.part_enat
data.nat.periodic
data.nat.pow
data.nat.prime
data.nat.psub
data.nat.sqrt
data.nat.sqrt_norm_num
data.nat.squarefree
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.algebra
data.pi.interval
data.pi.lex
data.pnat.basic
data.pnat.factors
data.pnat.find
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.expand
data.polynomial.field_division
data.polynomial.hasse_deriv
data.polynomial.identities
data.polynomial.induction
data.polynomial.inductions
data.polynomial.integral_normalization
data.polynomial.laurent
data.polynomial.lifts
data.polynomial.mirror
data.polynomial.module
data.polynomial.monic
data.polynomial.monomial
data.polynomial.reverse
data.polynomial.ring_division
data.polynomial.taylor
data.polynomial.unit_trinomial
data.prod.basic
data.prod.lex
data.prod.pprod
data.prod.tprod
data.psigma.order
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.defs
data.rat.denumerable
data.rat.floor
data.rat.meta_defs
data.rat.nnrat
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.constructions
data.set.countable
data.set.enumerate
data.set.equitable
data.set.finite
data.set.function
data.set.functor
data.set.intervals.basic
data.set.intervals.disjoint
data.set.intervals.image_preimage
data.set.intervals.infinite
data.set.intervals.instances
data.set.intervals.monotone
data.set.intervals.ord_connected
data.set.intervals.ord_connected_component
data.set.intervals.pi
data.set.intervals.proj_Icc
data.set.intervals.surj_on
data.set.intervals.unordered_interval
data.set.intervals.with_bot_top
data.set.lattice
data.set.opposite
data.set.pairwise
data.set.pointwise
data.set.prod
data.set.semiring
data.set.sigma
data.set_like.basic
data.set_like.fintype
data.setoid.basic
data.setoid.partition
data.sigma.basic
data.sigma.interval
data.sigma.lex
data.sigma.order
data.sign
data.stream.defs
data.stream.init
data.string.basic
data.string.defs
data.subtype
data.sum.basic
data.sum.interval
data.sum.order
data.sym.basic
data.sym.card
data.sym.sym2
data.tree
data.two_pointing
data.typevec
data.ulift
data.vector.basic
data.vector.mem
data.vector.zip
data.vector3
data.zmod.algebra
data.zmod.basic
data.zmod.coprime
data.zmod.defs
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.cardinality
field_theory.chevalley_warning
field_theory.finite.basic
field_theory.finite.galois_field
field_theory.finite.polynomial
field_theory.finite.trace
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.is_alg_closed.classification
field_theory.krull_topology
field_theory.laurent
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.inversion
geometry.euclidean.monge_point
geometry.euclidean.oriented_angle
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.bump_function
geometry.manifold.charted_space
geometry.manifold.complex
geometry.manifold.conformal_groupoid
geometry.manifold.cont_mdiff
geometry.manifold.cont_mdiff_map
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.metrizable
geometry.manifold.mfderiv
geometry.manifold.partition_of_unity
geometry.manifold.smooth_manifold_with_corners
geometry.manifold.tangent_bundle
geometry.manifold.whitney_embedding
group_theory.abelianization
group_theory.archimedean
group_theory.commensurable
group_theory.commutator
group_theory.commuting_probability
group_theory.complement
group_theory.congruence
group_theory.coset
group_theory.divisible
group_theory.double_coset
group_theory.eckmann_hilton
group_theory.exponent
group_theory.finite_abelian
group_theory.finiteness
group_theory.free_abelian_group
group_theory.free_abelian_group_finsupp
group_theory.free_group
group_theory.free_product
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.embedding
group_theory.group_action.fixing_subgroup
group_theory.group_action.group
group_theory.group_action.opposite
group_theory.group_action.option
group_theory.group_action.pi
group_theory.group_action.prod
group_theory.group_action.quotient
group_theory.group_action.sigma
group_theory.group_action.sub_mul_action
group_theory.group_action.sub_mul_action.pointwise
group_theory.group_action.sum
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.noncomm_pi_coprod
group_theory.order_of_element
group_theory.p_group
group_theory.perm.basic
group_theory.perm.cycle.basic
group_theory.perm.cycle.concrete
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.presented_group
group_theory.quotient_group
group_theory.schreier
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.centralizer
group_theory.submonoid.inverses
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.membership
group_theory.subsemigroup.operations
group_theory.sylow
group_theory.torsion
group_theory.transfer
information_theory.hamming
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.affine_space.pointwise
linear_algebra.affine_space.slope
linear_algebra.alternating
linear_algebra.annihilating_polynomial
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.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.coevaluation
linear_algebra.contraction
linear_algebra.cross_product
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.basic
linear_algebra.exterior_algebra.grading
linear_algebra.exterior_algebra.of_alternating
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.bilinear_form
linear_algebra.matrix.block
linear_algebra.matrix.charpoly.basic
linear_algebra.matrix.charpoly.coeff
linear_algebra.matrix.charpoly.finite_field
linear_algebra.matrix.charpoly.minpoly
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.hermitian
linear_algebra.matrix.invariant_basis_number
linear_algebra.matrix.is_diag
linear_algebra.matrix.ldl
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.pos_def
linear_algebra.matrix.reindex
linear_algebra.matrix.spectrum
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.finite_dimensional
linear_algebra.multilinear.tensor_product
linear_algebra.orientation
linear_algebra.pi
linear_algebra.pi_tensor_product
linear_algebra.prod
linear_algebra.projection
linear_algebra.projective_space.basic
linear_algebra.projective_space.independence
linear_algebra.projective_space.subspace
linear_algebra.quadratic_form.basic
linear_algebra.quadratic_form.complex
linear_algebra.quadratic_form.isometry
linear_algebra.quadratic_form.prod
linear_algebra.quadratic_form.real
linear_algebra.quotient
linear_algebra.ray
linear_algebra.sesquilinear_form
linear_algebra.smodeq
linear_algebra.span
linear_algebra.special_linear_group
linear_algebra.std_basis
linear_algebra.symplectic_group
linear_algebra.tensor_algebra.basic
linear_algebra.tensor_algebra.grading
linear_algebra.tensor_power
linear_algebra.tensor_product
linear_algebra.tensor_product_basis
linear_algebra.trace
linear_algebra.unitary_group
linear_algebra.vandermonde
logic.basic
logic.denumerable
logic.embedding
logic.encodable.basic
logic.encodable.lattice
logic.equiv.basic
logic.equiv.embedding
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.equiv.transfer_instance
logic.function.basic
logic.function.conjugate
logic.function.iterate
logic.hydra
logic.is_empty
logic.lemmas
logic.nonempty
logic.nontrivial
logic.relation
logic.relator
logic.small
logic.unique
measure_theory.card_measurable_space
measure_theory.category.Meas
measure_theory.constructions.borel_space
measure_theory.constructions.pi
measure_theory.constructions.polish
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.basic
measure_theory.function.conditional_expectation.indicator
measure_theory.function.conditional_expectation.real
measure_theory.function.continuous_map_dense
measure_theory.function.convergence_in_measure
measure_theory.function.egorov
measure_theory.function.ess_sup
measure_theory.function.floor
measure_theory.function.jacobian
measure_theory.function.l1_space
measure_theory.function.l2_space
measure_theory.function.locally_integrable
measure_theory.function.lp_order
measure_theory.function.lp_space
measure_theory.function.simple_func_dense
measure_theory.function.simple_func_dense_lp
measure_theory.function.special_functions
measure_theory.function.strongly_measurable
measure_theory.function.strongly_measurable_lp
measure_theory.function.uniform_integrable
measure_theory.group.action
measure_theory.group.arithmetic
measure_theory.group.fundamental_domain
measure_theory.group.integration
measure_theory.group.measurable_equiv
measure_theory.group.measure
measure_theory.group.pointwise
measure_theory.group.prod
measure_theory.integral.average
measure_theory.integral.bochner
measure_theory.integral.circle_integral
measure_theory.integral.circle_transform
measure_theory.integral.divergence_theorem
measure_theory.integral.exp_decay
measure_theory.integral.integrable_on
measure_theory.integral.integral_eq_improper
measure_theory.integral.interval_average
measure_theory.integral.interval_integral
measure_theory.integral.layercake
measure_theory.integral.lebesgue
measure_theory.integral.mean_inequalities
measure_theory.integral.periodic
measure_theory.integral.set_integral
measure_theory.integral.set_to_l1
measure_theory.integral.torus_integral
measure_theory.integral.vitali_caratheodory
measure_theory.lattice
measure_theory.measurable_space
measure_theory.measurable_space_def
measure_theory.measure.ae_disjoint
measure_theory.measure.ae_measurable
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.haar_quotient
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.open_pos
measure_theory.measure.outer_measure
measure_theory.measure.regular
measure_theory.measure.stieltjes
measure_theory.measure.sub
measure_theory.measure.vector_measure
measure_theory.measure.with_density_vector_measure
measure_theory.pi_system
measure_theory.tactic
meta.coinductive_predicates
meta.expr
meta.expr_lens
meta.rb_map
meta.uchange
meta.univs
model_theory.basic
model_theory.bundled
model_theory.definability
model_theory.direct_limit
model_theory.elementary_maps
model_theory.encoding
model_theory.finitely_generated
model_theory.fraisse
model_theory.graph
model_theory.language_map
model_theory.order
model_theory.quotients
model_theory.satisfiability
model_theory.semantics
model_theory.skolem
model_theory.substructures
model_theory.syntax
model_theory.types
model_theory.ultraproducts
number_theory.ADE_inequality
number_theory.arithmetic_function
number_theory.basic
number_theory.bernoulli
number_theory.bernoulli_polynomials
number_theory.bertrand
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.cyclotomic.basic
number_theory.cyclotomic.discriminant
number_theory.cyclotomic.gal
number_theory.cyclotomic.primitive_roots
number_theory.cyclotomic.rat
number_theory.dioph
number_theory.divisors
number_theory.fermat4
number_theory.frobenius_number
number_theory.function_field
number_theory.kummer_dedekind
number_theory.l_series
number_theory.legendre_symbol.add_character
number_theory.legendre_symbol.gauss_eisenstein_lemmas
number_theory.legendre_symbol.gauss_sum
number_theory.legendre_symbol.jacobi_symbol
number_theory.legendre_symbol.mul_character
number_theory.legendre_symbol.norm_num
number_theory.legendre_symbol.quadratic_char
number_theory.legendre_symbol.quadratic_reciprocity
number_theory.legendre_symbol.zmod_char
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.modular
number_theory.modular_forms.congruence_subgroups
number_theory.modular_forms.slash_actions
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.padic_val
number_theory.padics.ring_homs
number_theory.pell
number_theory.prime_counting
number_theory.primes_congruent_one
number_theory.primorial
number_theory.pythagorean_triples
number_theory.ramification_inertia
number_theory.sum_four_squares
number_theory.sum_two_squares
number_theory.von_mangoldt
number_theory.wilson
number_theory.zsqrtd.basic
number_theory.zsqrtd.gaussian_int
number_theory.zsqrtd.to_real
order.antichain
order.antisymmetrization
order.atoms
order.basic
order.boolean_algebra
order.bounded
order.bounded_order
order.bounds
order.category.BoolAlg
order.category.BoundedDistribLattice
order.category.BoundedLattice
order.category.BoundedOrder
order.category.CompleteLattice
order.category.DistribLattice
order.category.FinBoolAlg
order.category.FinPartialOrder
order.category.Frame
order.category.Lattice
order.category.LinearOrder
order.category.NonemptyFinLinOrd
order.category.PartialOrder
order.category.Preorder
order.category.Semilattice
order.category.omega_complete_partial_order
order.chain
order.circular
order.closure
order.compactly_generated
order.compare
order.complete_boolean_algebra
order.complete_lattice
order.complete_lattice_intervals
order.concept
order.conditionally_complete_lattice
order.copy
order.countable_dense_linear_order
order.cover
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.curry
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.n_ary
order.filter.partial
order.filter.pi
order.filter.pointwise
order.filter.prod
order.filter.small_sets
order.filter.ultrafilter
order.filter.zero_and_bounded_at_filter
order.fixed_points
order.galois_connection
order.game_add
order.grade
order.heyting.basic
order.heyting.boundary
order.heyting.regular
order.hom.basic
order.hom.bounded
order.hom.complete_lattice
order.hom.lattice
order.hom.order
order.ideal
order.initial_seg
order.interval
order.iterate
order.jordan_holder
order.lattice
order.lattice_intervals
order.liminf_limsup
order.locally_finite
order.max
order.min_max
order.minimal
order.modular_lattice
order.monotone
order.monovary
order.omega_complete_partial_order
order.ord_continuous
order.order_iso_nat
order.partial_sups
order.partition.equipartition
order.partition.finpartition
order.pfilter
order.prime_ideal
order.rel_classes
order.rel_iso
order.semiconj_Sup
order.succ_pred.basic
order.succ_pred.interval_succ
order.succ_pred.limit
order.succ_pred.relation
order.sup_indep
order.symm_diff
order.synonym
order.upper_lower
order.well_founded
order.well_founded_set
order.zorn
probability.cond_count
probability.conditional_expectation
probability.conditional_probability
probability.density
probability.ident_distrib
probability.independence
probability.integration
probability.martingale.basic
probability.martingale.borel_cantelli
probability.martingale.centering
probability.martingale.convergence
probability.martingale.optional_stopping
probability.martingale.upcrossing
probability.moments
probability.notation
probability.probability_mass_function.basic
probability.probability_mass_function.constructions
probability.probability_mass_function.monad
probability.probability_mass_function.uniform
probability.process.adapted
probability.process.filtration
probability.process.hitting_time
probability.process.stopping
probability.strong_law
probability.variance
representation_theory.Action
representation_theory.Rep
representation_theory.basic
representation_theory.character
representation_theory.fdRep
representation_theory.group_cohomology_resolution
representation_theory.invariants
representation_theory.maschke
ring_theory.adjoin.basic
ring_theory.adjoin.fg
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.bezout
ring_theory.chain_of_divisors
ring_theory.class_group
ring_theory.coprime.basic
ring_theory.coprime.ideal
ring_theory.coprime.lemmas
ring_theory.dedekind_domain.S_integer
ring_theory.dedekind_domain.adic_valuation
ring_theory.dedekind_domain.basic
ring_theory.dedekind_domain.dvr
ring_theory.dedekind_domain.ideal
ring_theory.dedekind_domain.integral_closure
ring_theory.derivation
ring_theory.discrete_valuation_ring
ring_theory.discriminant
ring_theory.eisenstein_criterion
ring_theory.etale
ring_theory.euclidean_domain
ring_theory.filtration
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.graded_algebra.homogeneous_ideal
ring_theory.graded_algebra.homogeneous_localization
ring_theory.graded_algebra.radical
ring_theory.hahn_series
ring_theory.henselian
ring_theory.ideal.basic
ring_theory.ideal.cotangent
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.is_tensor_product
ring_theory.jacobson
ring_theory.jacobson_ideal
ring_theory.laurent_series
ring_theory.local_properties
ring_theory.localization.as_subring
ring_theory.localization.at_prime
ring_theory.localization.away
ring_theory.localization.basic
ring_theory.localization.cardinality
ring_theory.localization.fraction_ring
ring_theory.localization.ideal
ring_theory.localization.integer
ring_theory.localization.integral
ring_theory.localization.inv_submonoid
ring_theory.localization.localization_localization
ring_theory.localization.module
ring_theory.localization.num_denom
ring_theory.localization.submodule
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.ore_localization.basic
ring_theory.ore_localization.ore_set
ring_theory.perfection
ring_theory.polynomial.basic
ring_theory.polynomial.bernstein
ring_theory.polynomial.chebyshev
ring_theory.polynomial.content
ring_theory.polynomial.cyclotomic.basic
ring_theory.polynomial.cyclotomic.eval
ring_theory.polynomial.dickson
ring_theory.polynomial.eisenstein
ring_theory.polynomial.gauss_lemma
ring_theory.polynomial.homogeneous
ring_theory.polynomial.opposites
ring_theory.polynomial.pochhammer
ring_theory.polynomial.rational_root
ring_theory.polynomial.scale_roots
ring_theory.polynomial.selmer
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.rees_algebra
ring_theory.ring_hom.finite
ring_theory.ring_hom.finite_type
ring_theory.ring_hom.integral
ring_theory.ring_hom_properties
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.extend_to_localization
ring_theory.valuation.integers
ring_theory.valuation.integral
ring_theory.valuation.valuation_ring
ring_theory.valuation.valuation_subring
ring_theory.witt_vector.basic
ring_theory.witt_vector.compare
ring_theory.witt_vector.defs
ring_theory.witt_vector.discrete_valuation_ring
ring_theory.witt_vector.domain
ring_theory.witt_vector.frobenius
ring_theory.witt_vector.frobenius_fraction_field
ring_theory.witt_vector.identities
ring_theory.witt_vector.init_tail
ring_theory.witt_vector.is_poly
ring_theory.witt_vector.isocrystal
ring_theory.witt_vector.mul_coeff
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.basic
set_theory.cardinal.cofinality
set_theory.cardinal.continuum
set_theory.cardinal.divisibility
set_theory.cardinal.finite
set_theory.cardinal.ordinal
set_theory.cardinal.schroeder_bernstein
set_theory.game.basic
set_theory.game.birthday
set_theory.game.domineering
set_theory.game.impartial
set_theory.game.nim
set_theory.game.ordinal
set_theory.game.pgame
set_theory.game.short
set_theory.game.state
set_theory.lists
set_theory.ordinal.arithmetic
set_theory.ordinal.basic
set_theory.ordinal.cantor_normal_form
set_theory.ordinal.fixed_point
set_theory.ordinal.natural_ops
set_theory.ordinal.notation
set_theory.ordinal.principal
set_theory.ordinal.topology
set_theory.surreal.basic
set_theory.surreal.dyadic
set_theory.zfc.basic
set_theory.zfc.ordinal
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.compute_degree
tactic.congr
tactic.congrm
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.expand_exists
tactic.explode
tactic.explode_widget
tactic.ext
tactic.field_simp
tactic.fin_cases
tactic.find
tactic.find_unused
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.local_cache
tactic.localized
tactic.mk_iff_of_inductive_prop
tactic.monotonicity.basic
tactic.monotonicity.interactive
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.observe
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.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.swap_var
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.const_mul_action
topology.algebra.constructions
topology.algebra.continuous_affine_map
topology.algebra.continuous_monoid_hom
topology.algebra.field
topology.algebra.filter_basis
topology.algebra.group
topology.algebra.group_completion
topology.algebra.group_with_zero
topology.algebra.infinite_sum
topology.algebra.localization
topology.algebra.module.basic
topology.algebra.module.character_space
topology.algebra.module.finite_dimension
topology.algebra.module.linear_pmap
topology.algebra.module.locally_convex
topology.algebra.module.multilinear
topology.algebra.module.weak_dual
topology.algebra.monoid
topology.algebra.mul_action
topology.algebra.nonarchimedean.adic_topology
topology.algebra.nonarchimedean.bases
topology.algebra.nonarchimedean.basic
topology.algebra.open_subgroup
topology.algebra.order.archimedean
topology.algebra.order.basic
topology.algebra.order.compact
topology.algebra.order.extend_from
topology.algebra.order.extr_closure
topology.algebra.order.floor
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.order.t5
topology.algebra.polynomial
topology.algebra.ring
topology.algebra.semigroup
topology.algebra.star
topology.algebra.uniform_convergence
topology.algebra.uniform_field
topology.algebra.uniform_filter_basis
topology.algebra.uniform_group
topology.algebra.uniform_mul_action
topology.algebra.uniform_ring
topology.algebra.valuation
topology.algebra.valued_field
topology.algebra.with_zero_topology
topology.bases
topology.basic
topology.bornology.basic
topology.bornology.constructions
topology.bornology.hom
topology.category.Born
topology.category.CompHaus.default
topology.category.CompHaus.projective
topology.category.Compactum
topology.category.Locale
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.connected
topology.constructions
topology.continuous_function.algebra
topology.continuous_function.basic
topology.continuous_function.bounded
topology.continuous_function.cocompact_map
topology.continuous_function.compact
topology.continuous_function.locally_constant
topology.continuous_function.ordered
topology.continuous_function.polynomial
topology.continuous_function.stone_weierstrass
topology.continuous_function.t0_sierpinski
topology.continuous_function.units
topology.continuous_function.weierstrass
topology.continuous_function.zero_at_infty
topology.continuous_on
topology.dense_embedding
topology.discrete_quotient
topology.extend_from
topology.fiber_bundle
topology.gluing
topology.hom.open
topology.homeomorph
topology.homotopy.basic
topology.homotopy.contractible
topology.homotopy.equiv
topology.homotopy.homotopy_group
topology.homotopy.path
topology.homotopy.product
topology.inseparable
topology.instances.discrete
topology.instances.ennreal
topology.instances.ereal
topology.instances.int
topology.instances.irrational
topology.instances.matrix
topology.instances.nat
topology.instances.nnreal
topology.instances.rat
topology.instances.rat_lemmas
topology.instances.real
topology.instances.real_vector_space
topology.instances.sign
topology.is_locally_homeomorph
topology.list
topology.local_at_target
topology.local_extr
topology.local_homeomorph
topology.locally_constant.algebra
topology.locally_constant.basic
topology.locally_finite
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.metrizable_uniformity
topology.metric_space.partition_of_unity
topology.metric_space.pi_nat
topology.metric_space.polish
topology.metric_space.shrinking_lemma
topology.metric_space.thickened_indicator
topology.nhds_set
topology.noetherian_space
topology.omega_complete_partial_order
topology.order
topology.order.hom.basic
topology.order.hom.esakia
topology.order.lattice
topology.order.priestley
topology.paracompact
topology.partition_of_unity
topology.path_connected
topology.quasi_separated
topology.semicontinuous
topology.separation
topology.sequences
topology.sets.closeds
topology.sets.compacts
topology.sets.opens
topology.sets.order
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.sober
topology.spectral.hom
topology.stone_cech
topology.subset_properties
topology.support
topology.tactic
topology.tietze_extension
topology.uniform_space.absolute_value
topology.uniform_space.abstract_completion
topology.uniform_space.basic
topology.uniform_space.cauchy
topology.uniform_space.compact
topology.uniform_space.compact_convergence
topology.uniform_space.compare_reals
topology.uniform_space.complete_separated
topology.uniform_space.completion
topology.uniform_space.equiv
topology.uniform_space.matrix
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
topology.urysohns_bounded
topology.urysohns_lemma
topology.vector_bundle.basic
topology.vector_bundle.hom
topology.vector_bundle.prod
topology.vector_bundle.pullback
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
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
mathlib
algebra
algebra
subalgebra
basic
pointwise
basic
bilinear
operations
restrict_scalars
spectrum
tower
unitization
big_operators
associated
basic
fin
finprod
finsupp
intervals
multiset
nat_antidiagonal
norm_num
option
order
part_enat
pi
ring
category
Algebra
basic
limits
FinVect
limits
Group
Z_Module_equivalence
abelian
adjunctions
basic
biproducts
colimits
epi_mono
equivalence_Group_AddGroup
filtered_colimits
images
limits
preadditive
subobject
zero
Module
abelian
adjunctions
basic
biproducts
change_of_rings
colimits
epi_mono
filtered_colimits
images
kernels
limits
monoidal
products
projective
simple
subobject
tannaka
Mon
adjunctions
basic
colimits
filtered_colimits
limits
Ring
adjunctions
basic
colimits
constructions
filtered_colimits
instances
limits
Semigroup
basic
BoolRing
FinVect
GroupWithZero
char_p
algebra
basic
char_and_card
exp_char
invertible
local_ring
pi
quotient
subring
two
char_zero
defs
quotient
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
decomposition
finsupp
internal
module
ring
field
basic
opposite
gcd_monoid
basic
finset
integrally_closed
multiset
nat
group
basic
commute
conj
default
defs
ext
inj_surj
opposite
pi
prod
semiconj
to_additive
type_tags
ulift
units
with_one
group_power
basic
identities
lemmas
order
ring
group_with_zero
basic
defs
power
hom
aut
centroid
equiv
freiman
group
group_action
group_instances
iterate
non_unital_alg
ring
units
homology
short_exact
abelian
preadditive
Module
additive
augment
complex_shape
differential_object
exact
flip
functor
homological_complex
homology
homotopy
homotopy_category
image_to_kernel
quasi_iso
single
jordan
basic
lie
abelian
base_change
basic
cartan_matrix
cartan_subalgebra
centralizer
character
classical
direct_sum
engel
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
submodule
basic
bilinear
lattice
pointwise
algebra
basic
bimodule
dedekind_domain
default
equiv
hom
injective
linear_map
localized_module
opposites
pi
pid
pointwise_pi
prod
projective
torsion
ulift
monoid_algebra
basic
degree
grading
no_zero_divisors
support
to_direct_sum
order
hom
basic
monoid
ring
positive
field
ring
absolute_value
algebra
archimedean
complete_field
euclidean_absolute_value
field
field_defs
floor
group
invertible
lattice_group
module
monoid
monoid_lemmas
monoid_lemmas_zero_lt
nonneg
pi
pointwise
rearrangement
ring
smul
sub
to_interval_mod
with_zero
polynomial
big_operators
group_ring_action
regular
basic
pow
smul
ring
aut
basic
boolean_ring
comp_typeclasses
default
equiv
idempotents
opposite
pi
prod
ulift
star
basic
chsh
free
module
pi
pointwise
prod
self_adjoint
star_alg_hom
subalgebra
unitary
tropical
basic
big_operators
lattice
abs
add_torsor
algebraic_card
associated
bounds
char_zero
covariant_and_contravariant
cubic_discriminant
direct_limit
divisibility
dual_number
euclidean_domain
free
free_algebra
free_monoid
free_non_unital_non_assoc_algebra
geom_sum
graded_monoid
group_ring_action
hierarchy_design
indicator_function
invertible
is_prime_pow
linear_recurrence
ne_zero
opposites
parity
pempty_instances
periodic
punit_instances
quadratic_discriminant
quandle
quaternion
quaternion_basis
quotient
ring_quot
smul_with_zero
squarefree
support
symmetrized
triv_sq_zero_ext
algebraic_geometry
locally_ringed_space
has_colimits
morphisms
basic
quasi_compact
ring_hom_properties
presheafed_space
gluing
has_colimits
prime_spectrum
basic
is_open_comap_C
noetherian
projective_spectrum
scheme
structure_sheaf
topology
AffineScheme
EllipticCurve
Gamma_Spec_adjunction
Scheme
Spec
function_field
gluing
limits
locally_ringed_space
open_immersion
presheafed_space
properties
pullbacks
ringed_space
sheafed_space
stalks
structure_sheaf
algebraic_topology
dold_kan
faces
functor_n
homotopies
homotopy_equivalence
normalized
notations
p_infty
projections
fundamental_groupoid
basic
fundamental_group
induced_maps
product
punit
simply_connected
Moore_complex
alternating_face_map_complex
cech_nerve
nerve
simplex_category
simplicial_object
simplicial_set
split_simplicial_object
topological_simplex
analysis
ODE
gronwall
picard_lindelof
analytic
basic
composition
inverse
isolated_zeros
linear
radius_liminf
asymptotics
asymptotic_equivalent
asymptotics
specific_asymptotics
superpolynomial_decay
theta
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
cont_diff
darboux
deriv
diff_on_int_cont
dslope
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
taylor
uniform_limits_deriv
complex
upper_half_plane
basic
functions_bounded_at_infty
metric
topology
abs_max
arg
basic
cauchy_integral
circle
conformal
isometry
liouville
phragmen_lindelof
polynomial
re_im_topology
real_deriv
removable_singularity
roots_of_unity
schwarz
convex
cone
basic
simplicial_complex
basic
basic
caratheodory
combination
complex
contractible
exposed
extrema
extreme
function
gauge
hull
independent
integral
jensen
join
krein_milman
measure
partition_of_unity
quasiconvex
segment
slope
specific_functions
star
stone_separation
strict
strict_convex_space
topology
uniform
inner_product_space
adjoint
basic
calculus
conformal_linear_map
dual
euclidean_dist
gram_schmidt_ortho
l2_space
lax_milgram
orientation
pi_L2
positive
projection
rayleigh
spectrum
symmetric
locally_convex
balanced_core_hull
basic
bounded
polar
weak_dual
with_seminorms
normed
field
basic
unit_ball
group
SemiNormedGroup
completion
kernels
SemiNormedGroup
add_torsor
ball_sphere
basic
completion
hom
hom_completion
infinite_sum
pointwise
quotient
seminorm
ring
seminorm
normed_space
hahn_banach
extension
separation
star
basic
complex
exponential
gelfand_duality
matrix
spectrum
M_structure
add_torsor
add_torsor_bases
affine_isometry
algebra
ball_action
banach
banach_steinhaus
basic
bounded_linear_maps
compact_operator
complemented
completion
conformal_linear_map
continuous_affine_map
dual
enorm
exponential
extend
extr
finite_dimension
indicator_function
int
is_R_or_C
lattice_ordered_group
linear_isometry
lp_space
matrix_exponential
mazur_ulam
multilinear
operator_norm
ordered
pi_Lp
pointwise
ray
riesz_lemma
spectrum
units
weak_dual
special_functions
complex
arg
circle
log
log_deriv
log
base
basic
deriv
monotone
trigonometric
angle
arctan
arctan_deriv
basic
bounds
chebyshev
complex
complex_deriv
deriv
inverse
inverse_deriv
arsinh
bernstein
compare_exp
exp
exp_deriv
exponential
gamma
gaussian
integrals
non_integrable
polar_coord
polynomials
pow
pow_deriv
sqrt
stirling
specific_limits
basic
floor_pow
normed
von_neumann_algebra
basic
convolution
fourier
hofer
matrix
mean_inequalities
mean_inequalities_pow
p_series
quaternion
schwartz_space
seminorm
subadditive
sum_integral_comparisons
category_theory
abelian
diagram_lemmas
four
basic
exact
ext
functor_category
generator
homology
images
injective_resolution
left_derived
non_preadditive
opposite
projective
pseudoelements
right_derived
subobject
transfer
additive
basic
adjunction
adjoint_functor_theorems
basic
comma
evaluation
fully_faithful
lifting
limits
mates
opposites
over
reflective
whiskering
bicategory
End
basic
coherence
coherence_tactic
free
functor
functor_bicategory
locally_discrete
natural_transformation
single_obj
strict
category
Cat
limit
Bipointed
Cat
Groupoid
Kleisli
PartialFun
Pointed
Quiv
Rel
Twop
basic
pairwise
preorder
ulift
closed
cartesian
functor
ideal
monoidal
types
zero
concrete_category
basic
bundled
bundled_hom
elementwise
reflects_isomorphisms
unbundled_hom
endofunctor
algebra
enriched
basic
functor
basic
category
const
currying
epi_mono
flat
fully_faithful
functorial
hom
inv_isos
left_derived
reflects_isomorphisms
idempotents
basic
biproducts
functor_categories
functor_extension
karoubi
karoubi_karoubi
simplicial_object
lifting_properties
adjunction
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
biproducts
equalizers
images
kernels
products
pullbacks
terminal
zero
basic
filtered
finite
functor_category
limits
opposites
shapes
normal_mono
basic
equalizers
binary_products
biproducts
comm_sq
concrete_category
diagonal
disjoint_coproduct
equalizers
equivalence
finite_limits
finite_products
functor_category
images
kernel_pair
kernels
multiequalizer
products
pullbacks
reflexive
regular_mono
split_coequalizer
strict_initial
strong_epi
terminal
types
wide_equalizers
wide_pullbacks
zero_morphisms
zero_objects
bicones
colimit_limit
comma
concrete_category
cone_category
cones
connected
creates
essentially_small
exact_functor
filtered_colimit_commutes_finite_limit
final
fubini
full_subcategory
functor_category
has_limits
is_limit
kan_extension
lattice
opposites
over
pi
presheaf
small_complete
types
unit
yoneda
linear
default
functor_category
linear_functor
yoneda
localization
construction
monad
adjunction
algebra
basic
coequalizer
equiv_mon
kleisli
limits
monadicity
products
types
monoidal
free
basic
coherence
internal
Module
functor_category
limits
types
rigid
basic
functor_category
of_equivalence
CommMon_
End
Mod
Mon_
braided
category
center
coherence
coherence_lemmas
discrete
functor
functor_category
functorial
limits
linear
natural_transformation
of_chosen_finite_products
of_has_finite_products
opposite
preadditive
skeleton
subcategory
tor
transport
types
pi
basic
preadditive
Mat
additive_functor
biproducts
default
eilenberg_moore
endo_functor
functor_category
generator
hom_orthogonal
injective
injective_resolution
left_exact
of_biproducts
opposite
projective
projective_resolution
schur
single_obj
yoneda
products
associator
basic
bifunctor
sigma
basic
sites
adjunction
canonical
closed
compatible_plus
compatible_sheafification
cover_lifting
cover_preserving
dense_subsite
grothendieck
induced_topology
left_exact
limits
plus
pretopology
sheaf
sheaf_of_types
sheafification
sieves
spaces
subsheaf
types
whiskering
subobject
basic
comma
factor_thru
lattice
limits
mono_over
types
well_powered
sums
associator
basic
triangulated
basic
pretriangulated
rotate
Fintype
action
arrow
balanced
comm_sq
comma
conj
connected_components
core
differential_object
discrete_category
elements
elementwise
endomorphism
epi_mono
eq_to_hom
equivalence
essential_image
essentially_small
filtered
fin_category
full_subcategory
generator
glue_data
graded_object
grothendieck
groupoid
is_connected
isomorphism
isomorphism_classes
morphism_property
natural_isomorphism
natural_transformation
noetherian
opposites
over
path_category
pempty
punit
quotient
shift
simple
single_obj
skeletal
structured_arrow
subterminal
thin
types
whiskering
with_terminal
yoneda
combinatorics
additive
behrend
pluennecke_ruzsa
ruzsa_covering
salem_spencer
derangements
basic
exponential
finite
hall
basic
finite
quiver
arborescence
basic
connected_component
path
subquiver
set_family
compression
down
uv
harris_kleitman
intersecting
kleitman
lym
shadow
simple_graph
regularity
bound
energy
equitabilise
uniform
triangle
basic
adj_matrix
basic
clique
coloring
connectivity
degree_sum
density
hasse
inc_matrix
matching
metric
partition
prod
strongly_regular
subgraph
trails
catalan
colex
composition
configuration
double_counting
hales_jewett
hindman
partition
pigeonhole
young_diagram
computability
DFA
NFA
ackermann
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
constructions
analysis
filter
topology
array
lemmas
bitvec
basic
core
bool
all_any
basic
set
buffer
parser
basic
numeral
basic
complex
basic
cardinality
determinant
exponential
exponential_bounds
is_R_or_C
module
countable
basic
defs
small
dfinsupp
basic
interval
order
dlist
basic
instances
fin
tuple
basic
monotone
nat_antidiagonal
sort
basic
fin2
interval
succ_pred
vec_notation
finite
basic
card
defs
set
finset
basic
card
fin
finsupp
fold
functor
interval
lattice
locally_finite
n_ary
nat_antidiagonal
noncomm_prod
option
order
pairwise
pi
pi_induction
pimage
pointwise
powerset
preimage
prod
sigma
slice
sort
sum
sym
finsupp
antidiagonal
basic
big_operators
default
defs
fin
indicator
interval
lex
multiset
ne_locus
order
pointwise
pwo
to_dfinsupp
fintype
basic
card
card_embedding
fin
list
order
small
sort
fp
basic
fun_like
basic
embedding
equiv
int
cast
defs
absolute_value
basic
cast
cast_field
char_zero
gcd
interval
least_greatest
log
modeq
nat_prime
order
parity
range
sqrt
succ_pred
lazy_list
basic
list
alist
basic
big_operators
chain
count
cycle
dedup
defs
destutter
duplicate
forall2
func
indexes
infix
intervals
join
lattice
lex
min_max
nat_antidiagonal
nodup
nodup_equiv_fin
of_fn
pairwise
palindrome
perm
permutation
prime
prod_sigma
range
rdrop
rotate
sections
sigma
sort
sublists
tfae
zip
matrix
basic
basis
block
char_p
dmatrix
hadamard
kronecker
notation
pequiv
rank
multiset
antidiagonal
basic
bind
dedup
finset_ops
fintype
fold
functor
lattice
locally_finite
nat_antidiagonal
nodup
pi
powerset
range
sections
sort
sum
mv_polynomial
basic
cardinal
comap
comm_ring
counit
derivation
equiv
expand
funext
invertible
monad
pderiv
rename
supported
variables
nat
cast
defs
choose
basic
bounds
cast
central
dvd
factorization
multinomial
sum
vandermonde
factorial
basic
big_operators
cast
factorization
basic
prime_pow
basic
bits
bitwise
cast
cast_field
count
digits
dist
enat
fib
gcd
interval
lattice
log
modeq
multiplicity
nth
pairing
parity
part_enat
periodic
pow
prime
psub
sqrt
sqrt_norm_num
squarefree
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
pi
algebra
interval
lex
pnat
basic
factors
find
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
expand
field_division
hasse_deriv
identities
induction
inductions
integral_normalization
laurent
lifts
mirror
module
monic
monomial
reverse
ring_division
taylor
unit_trinomial
prod
basic
lex
pprod
tprod
psigma
order
qpf
multivariate
constructions
cofix
comp
const
fix
prj
quot
sigma
basic
univariate
basic
rat
basic
cast
default
defs
denumerable
floor
meta_defs
nnrat
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
instances
monotone
ord_connected
ord_connected_component
pi
proj_Icc
surj_on
unordered_interval
with_bot_top
Union_lift
accumulate
basic
constructions
countable
enumerate
equitable
finite
function
functor
lattice
opposite
pairwise
pointwise
prod
semiring
sigma
set_like
basic
fintype
setoid
basic
partition
sigma
basic
interval
lex
order
stream
defs
init
string
basic
defs
sum
basic
interval
order
sym
basic
card
sym2
vector
basic
mem
zip
zmod
algebra
basic
coprime
defs
parity
quotient
bracket
bundle
char
erased
fin_enum
finmap
hash_map
holor
json
lazy_list
mllist
opposite
part
pequiv
pfun
quot
rel
semiquot
sign
subtype
tree
two_pointing
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
trace
is_alg_closed
algebraic_closure
basic
classification
abel_ruffini
adjoin
cardinality
chevalley_warning
finiteness
fixed
galois
intermediate_field
krull_topology
laurent
minpoly
mv_polynomial
normal
perfect_closure
polynomial_galois_group
primitive_element
ratfunc
separable
separable_degree
splitting_field
subfield
tower
geometry
euclidean
basic
circumcenter
inversion
monge_point
oriented_angle
sphere
triangle
manifold
algebra
left_invariant_derivation
lie_group
monoid
smooth_functions
structures
instances
real
sphere
units_of_normed_algebra
bump_function
charted_space
complex
conformal_groupoid
cont_mdiff
cont_mdiff_map
derivation_bundle
diffeomorph
local_invariant_properties
metrizable
mfderiv
partition_of_unity
smooth_manifold_with_corners
tangent_bundle
whitney_embedding
group_theory
group_action
sub_mul_action
pointwise
basic
big_operators
conj_act
defs
embedding
fixing_subgroup
group
opposite
option
pi
prod
quotient
sigma
sub_mul_action
sum
units
perm
cycle
basic
concrete
type
basic
fin
list
option
sign
subgroup
support
specific_groups
alternating
cyclic
dihedral
quaternion
subgroup
basic
pointwise
submonoid
basic
center
centralizer
inverses
membership
operations
pointwise
subsemigroup
basic
center
centralizer
membership
operations
abelianization
archimedean
commensurable
commutator
commuting_probability
complement
congruence
coset
divisible
double_coset
eckmann_hilton
exponent
finite_abelian
finiteness
free_abelian_group
free_abelian_group_finsupp
free_group
free_product
index
is_free_group
monoid_localization
nielsen_schreier
nilpotent
noncomm_pi_coprod
order_of_element
p_group
presented_group
quotient_group
schreier
schur_zassenhaus
semidirect_product
solvable
sylow
torsion
transfer
information_theory
hamming
linear_algebra
affine_space
affine_equiv
affine_map
affine_subspace
basic
basis
combination
finite_dimensional
independent
midpoint
ordered
pointwise
slope
charpoly
basic
to_matrix
clifford_algebra
basic
conjugation
equivs
even
even_equiv
fold
grading
star
direct_sum
finsupp
tensor_product
exterior_algebra
basic
grading
of_alternating
free_module
finite
basic
rank
basic
pid
rank
strong_rank_condition
matrix
charpoly
basic
coeff
finite_field
minpoly
absolute_value
adjugate
basis
bilinear_form
block
circulant
determinant
diagonal
dot_product
dual
finite_dimensional
hermitian
invariant_basis_number
is_diag
ldl
mv_polynomial
nondegenerate
nonsingular_inverse
orthogonal
polynomial
pos_def
reindex
spectrum
symmetric
to_lin
to_linear_equiv
trace
transvection
zpow
multilinear
basic
basis
finite_dimensional
tensor_product
projective_space
basic
independence
subspace
quadratic_form
basic
complex
isometry
prod
real
tensor_algebra
basic
grading
adic_completion
alternating
annihilating_polynomial
basic
basis
bilinear_form
bilinear_map
coevaluation
contraction
cross_product
determinant
dfinsupp
dimension
dual
eigenspace
finite_dimensional
finsupp
finsupp_vector_space
free_algebra
general_linear_group
invariant_basis_number
isomorphisms
lagrange
linear_independent
linear_pmap
orientation
pi
pi_tensor_product
prod
projection
quotient
ray
sesquilinear_form
smodeq
span
special_linear_group
std_basis
symplectic_group
tensor_power
tensor_product
tensor_product_basis
trace
unitary_group
vandermonde
logic
encodable
basic
lattice
equiv
basic
embedding
fin
fintype
functor
list
local_equiv
nat
option
set
transfer_instance
function
basic
conjugate
iterate
basic
denumerable
embedding
hydra
is_empty
lemmas
nonempty
nontrivial
relation
relator
small
unique
measure_theory
category
Meas
constructions
borel_space
pi
polish
prod
covering
besicovitch
besicovitch_vector_space
differentiation
vitali
vitali_family
decomposition
jordan
lebesgue
radon_nikodym
signed_hahn
unsigned_hahn
function
conditional_expectation
basic
indicator
real
ae_eq_fun
ae_eq_of_integral
ae_measurable_order
ae_measurable_sequence
continuous_map_dense
convergence_in_measure
egorov
ess_sup
floor
jacobian
l1_space
l2_space
locally_integrable
lp_order
lp_space
simple_func_dense
simple_func_dense_lp
special_functions
strongly_measurable
strongly_measurable_lp
uniform_integrable
group
action
arithmetic
fundamental_domain
integration
measurable_equiv
measure
pointwise
prod
integral
average
bochner
circle_integral
circle_transform
divergence_theorem
exp_decay
integrable_on
integral_eq_improper
interval_average
interval_integral
layercake
lebesgue
mean_inequalities
periodic
set_integral
set_to_l1
torus_integral
vitali_caratheodory
measure
ae_disjoint
ae_measurable
complex
complex_lebesgue
content
finite_measure_weak_convergence
giry_monad
haar
haar_lebesgue
haar_quotient
hausdorff
lebesgue
measure_space
measure_space_def
mutually_singular
null_measurable
open_pos
outer_measure
regular
stieltjes
sub
vector_measure
with_density_vector_measure
card_measurable_space
lattice
measurable_space
measurable_space_def
pi_system
tactic
meta
coinductive_predicates
expr
expr_lens
rb_map
uchange
univs
model_theory
basic
bundled
definability
direct_limit
elementary_maps
encoding
finitely_generated
fraisse
graph
language_map
order
quotients
satisfiability
semantics
skolem
substructures
syntax
types
ultraproducts
number_theory
class_number
admissible_abs
admissible_absolute_value
admissible_card_pow_degree
finite
function_field
number_field
cyclotomic
basic
discriminant
gal
primitive_roots
rat
legendre_symbol
add_character
gauss_eisenstein_lemmas
gauss_sum
jacobi_symbol
mul_character
norm_num
quadratic_char
quadratic_reciprocity
zmod_char
liouville
basic
liouville_constant
liouville_with
measure
residual
modular_forms
congruence_subgroups
slash_actions
padics
hensel
padic_integers
padic_norm
padic_numbers
padic_val
ring_homs
zsqrtd
basic
gaussian_int
to_real
ADE_inequality
arithmetic_function
basic
bernoulli
bernoulli_polynomials
bertrand
dioph
divisors
fermat4
frobenius_number
function_field
kummer_dedekind
l_series
lucas_lehmer
lucas_primality
modular
number_field
pell
prime_counting
primes_congruent_one
primorial
pythagorean_triples
ramification_inertia
sum_four_squares
sum_two_squares
von_mangoldt
wilson
order
category
BoolAlg
BoundedDistribLattice
BoundedLattice
BoundedOrder
CompleteLattice
DistribLattice
FinBoolAlg
FinPartialOrder
Frame
Lattice
LinearOrder
NonemptyFinLinOrd
PartialOrder
Preorder
Semilattice
omega_complete_partial_order
filter
archimedean
at_top_bot
bases
basic
cofinite
countable_Inter
curry
ennreal
extr
filter_product
germ
indicator_function
interval
lift
modeq
n_ary
partial
pi
pointwise
prod
small_sets
ultrafilter
zero_and_bounded_at_filter
heyting
basic
boundary
regular
hom
basic
bounded
complete_lattice
lattice
order
partition
equipartition
finpartition
succ_pred
basic
interval_succ
limit
relation
antichain
antisymmetrization
atoms
basic
boolean_algebra
bounded
bounded_order
bounds
chain
circular
closure
compactly_generated
compare
complete_boolean_algebra
complete_lattice
complete_lattice_intervals
concept
conditionally_complete_lattice
copy
countable_dense_linear_order
cover
directed
disjointed
extension
fixed_points
galois_connection
game_add
grade
ideal
initial_seg
interval
iterate
jordan_holder
lattice
lattice_intervals
liminf_limsup
locally_finite
max
min_max
minimal
modular_lattice
monotone
monovary
omega_complete_partial_order
ord_continuous
order_iso_nat
partial_sups
pfilter
prime_ideal
rel_classes
rel_iso
semiconj_Sup
sup_indep
symm_diff
synonym
upper_lower
well_founded
well_founded_set
zorn
probability
martingale
basic
borel_cantelli
centering
convergence
optional_stopping
upcrossing
probability_mass_function
basic
constructions
monad
uniform
process
adapted
filtration
hitting_time
stopping
cond_count
conditional_expectation
conditional_probability
density
ident_distrib
independence
integration
moments
notation
strong_law
variance
representation_theory
Action
Rep
basic
character
fdRep
group_cohomology_resolution
invariants
maschke
ring_theory
adjoin
basic
fg
power_basis
coprime
basic
ideal
lemmas
dedekind_domain
S_integer
adic_valuation
basic
dvr
ideal
integral_closure
graded_algebra
basic
homogeneous_ideal
homogeneous_localization
radical
ideal
basic
cotangent
local_ring
operations
over
prod
quotient
int
basic
localization
as_subring
at_prime
away
basic
cardinality
fraction_ring
ideal
integer
integral
inv_submonoid
localization_localization
module
num_denom
submodule
mv_polynomial
basic
ore_localization
basic
ore_set
polynomial
cyclotomic
basic
eval
basic
bernstein
chebyshev
content
dickson
eisenstein
gauss_lemma
homogeneous
opposites
pochhammer
rational_root
scale_roots
selmer
symmetric
tower
vieta
power_series
basic
well_known
ring_hom
finite
finite_type
integral
subring
basic
pointwise
subsemiring
basic
pointwise
valuation
basic
extend_to_localization
integers
integral
valuation_ring
valuation_subring
witt_vector
basic
compare
defs
discrete_valuation_ring
domain
frobenius
frobenius_fraction_field
identities
init_tail
is_poly
isocrystal
mul_coeff
mul_p
structure_polynomial
teichmuller
truncated
verschiebung
witt_polynomial
adjoin_root
algebra_tower
algebraic
algebraic_independent
artinian
bezout
chain_of_divisors
class_group
derivation
discrete_valuation_ring
discriminant
eisenstein_criterion
etale
euclidean_domain
filtration
finiteness
fintype
flat
fractional_ideal
free_comm_ring
free_ring
hahn_series
henselian
integral_closure
integral_domain
integrally_closed
is_tensor_product
jacobson
jacobson_ideal
laurent_series
local_properties
matrix_algebra
multiplicity
nakayama
nilpotent
noetherian
non_zero_divisors
norm
nullstellensatz
perfection
polynomial_algebra
power_basis
prime
principal_ideal_domain
rees_algebra
ring_hom_properties
ring_invo
roots_of_unity
simple_module
tensor_product
trace
unique_factorization_domain
set_theory
cardinal
basic
cofinality
continuum
divisibility
finite
ordinal
schroeder_bernstein
game
basic
birthday
domineering
impartial
nim
ordinal
pgame
short
state
ordinal
arithmetic
basic
cantor_normal_form
fixed_point
natural_ops
notation
principal
topology
surreal
basic
dyadic
zfc
basic
ordinal
lists
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
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
compute_degree
congr
congrm
core
dec_trivial
delta_instance
dependencies
derive_fintype
derive_inhabited
doc_commands
elementwise
elide
equiv_rw
expand_exists
explode
explode_widget
ext
field_simp
fin_cases
find
find_unused
finish
fresh_names
generalize_proofs
generalizes
group
has_variable_names
hint
induction
interactive
interactive_expr
interval_cases
itauto
lean_core_docs
lift
linear_combination
local_cache
localized
mk_iff_of_inductive_prop
noncomm_ring
norm_cast
norm_fin
norm_num
norm_swap
observe
obviously
pi_instances
polyrith
positivity
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
swap_var
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
module
basic
character_space
finite_dimension
linear_pmap
locally_convex
multilinear
weak_dual
nonarchimedean
adic_topology
bases
basic
order
archimedean
basic
compact
extend_from
extr_closure
floor
intermediate_value
left_right
liminf_limsup
monotone_continuity
monotone_convergence
proj_Icc
t5
affine
algebra
const_mul_action
constructions
continuous_affine_map
continuous_monoid_hom
field
filter_basis
group
group_completion
group_with_zero
infinite_sum
localization
monoid
mul_action
open_subgroup
polynomial
ring
semigroup
star
uniform_convergence
uniform_field
uniform_filter_basis
uniform_group
uniform_mul_action
uniform_ring
valuation
valued_field
with_zero_topology
bornology
basic
constructions
hom
category
CompHaus
default
projective
Profinite
as_limit
cofiltered_limit
default
projective
Top
adjunctions
basic
epi_mono
limits
open_nhds
opens
Born
Compactum
Locale
TopCommRing
UniformSpace
continuous_function
algebra
basic
bounded
cocompact_map
compact
locally_constant
ordered
polynomial
stone_weierstrass
t0_sierpinski
units
weierstrass
zero_at_infty
hom
open
homotopy
basic
contractible
equiv
homotopy_group
path
product
instances
discrete
ennreal
ereal
int
irrational
matrix
nat
nnreal
rat
rat_lemmas
real
real_vector_space
sign
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
metrizable_uniformity
partition_of_unity
pi_nat
polish
shrinking_lemma
thickened_indicator
order
hom
basic
esakia
lattice
priestley
sets
closeds
compacts
opens
order
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
spectral
hom
uniform_space
absolute_value
abstract_completion
basic
cauchy
compact
compact_convergence
compare_reals
complete_separated
completion
equiv
matrix
pi
separation
uniform_convergence
uniform_convergence_topology
uniform_embedding
vector_bundle
basic
hom
prod
pullback
G_delta
alexandroff
bases
basic
compact_open
connected
constructions
continuous_on
dense_embedding
discrete_quotient
extend_from
fiber_bundle
gluing
homeomorph
inseparable
is_locally_homeomorph
list
local_at_target
local_extr
local_homeomorph
locally_finite
maps
nhds_set
noetherian_space
omega_complete_partial_order
order
paracompact
partition_of_unity
path_connected
quasi_separated
semicontinuous
separation
sequences
shrinking_lemma
sober
stone_cech
subset_properties
support
tactic
tietze_extension
unit_interval
urysohns_bounded
urysohns_lemma
Color scheme
dark
system
light