mathlib3
documentation
simplification
Google site search
simplification
Simp
#
This page has moved to the
leanprover-community website
.
General documentation
index
foundational types
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
tower
basic
bilinear
equiv
hom
operations
pi
prod
restrict_scalars
spectrum
tower
unitization
big_operators
multiset
basic
lemmas
associated
basic
fin
finprod
finsupp
intervals
nat_antidiagonal
norm_num
option
order
pi
ring
ring_equiv
category
Algebra
basic
limits
Group
Z_Module_equivalence
abelian
adjunctions
basic
biproducts
colimits
epi_mono
equivalence_Group_AddGroup
filtered_colimits
images
injective
limits
preadditive
subobject
zero
Module
monoidal
basic
closed
symmetric
abelian
adjunctions
algebra
basic
biproducts
change_of_rings
colimits
epi_mono
filtered_colimits
images
kernels
limits
products
projective
simple
subobject
tannaka
Mon
adjunctions
basic
colimits
filtered_colimits
limits
Ring
adjunctions
basic
colimits
constructions
filtered_colimits
instances
limits
Semigroup
basic
fgModule
basic
limits
BoolRing
GroupWithZero
char_p
algebra
basic
char_and_card
exp_char
invertible
local_ring
mixed_char_zero
pi
quotient
subring
two
char_zero
defs
infinite
lemmas
quotient
continued_fractions
computation
approximation_corollaries
approximations
basic
correctness_terminating
terminates_iff_rat
translations
basic
continuants_recurrence
convergents_equiv
terminated_stable
translations
direct_sum
algebra
basic
decomposition
finsupp
internal
module
ring
divisibility
basic
units
euclidean_domain
basic
defs
instances
field
basic
defs
opposite
power
ulift
free_monoid
basic
count
gcd_monoid
basic
div
finset
integrally_closed
multiset
group
with_one
basic
defs
units
basic
commutator
commute
conj
conj_finite
defs
ext
inj_surj
opposite
order_synonym
pi
prod
semiconj
type_tags
ulift
unique_prods
units
group_power
basic
identities
lemmas
order
ring
group_ring_action
basic
invariant
subobjects
group_with_zero
units
basic
lemmas
basic
commute
defs
divisibility
inj_surj
power
semiconj
hom
equiv
units
basic
group_with_zero
basic
type_tags
aut
centroid
commute
embedding
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
local_cohomology
opposite
quasi_iso
single
jordan
basic
lie
abelian
base_change
basic
cartan_matrix
cartan_subalgebra
character
classical
direct_sum
engel
free
ideal_operations
matrix
nilpotent
non_unital_non_assoc_algebra
normalizer
of_associative
quotient
semisimple
skew_adjoint
solvable
subalgebra
submodule
tensor_product
universal_enveloping
weights
module
submodule
basic
bilinear
lattice
pointwise
algebra
basic
big_operators
bimodule
dedekind_domain
equiv
graded_module
hom
injective
linear_map
localized_module
opposites
pi
pid
pointwise_pi
prod
projective
torsion
ulift
zlattice
monoid_algebra
basic
degree
division
grading
ideal
no_zero_divisors
support
to_direct_sum
order
field
canonical
basic
defs
basic
defs
inj_surj
pi
power
group
abs
bounds
defs
densely_ordered
inj_surj
instances
min_max
order_iso
prod
type_tags
units
with_top
hom
basic
monoid
ring
monoid
cancel
basic
defs
canonical
defs
with_zero
basic
defs
basic
defs
lemmas
min_max
nat_cast
order_dual
prod
to_mul_bot
type_tags
units
with_top
nonneg
field
floor
ring
positive
field
ring
ring
abs
canonical
char_zero
cone
defs
inj_surj
lemmas
with_top
sub
basic
canonical
defs
with_top
absolute_value
algebra
archimedean
chebyshev
complete_field
euclidean_absolute_value
floor
interval
invertible
kleene
lattice_group
module
pi
pointwise
rearrangement
smul
to_interval_mod
upper_lower
with_zero
zero_le_one
polynomial
big_operators
group_ring_action
regular
basic
pow
smul
ring
add_aut
aut
basic
boolean_ring
commute
comp_typeclasses
defs
divisibility
equiv
fin
idempotents
inj_surj
opposite
order_synonym
pi
prod
regular
semiconj
ulift
units
star
basic
big_operators
chsh
free
module
order
pi
pointwise
prod
self_adjoint
star_alg_hom
subalgebra
unitary
tropical
basic
big_operators
lattice
abs
add_torsor
algebraic_card
associated
bounds
covariant_and_contravariant
cubic_discriminant
direct_limit
dual_number
dual_quaternion
expr
free
free_algebra
free_non_unital_non_assoc_algebra
geom_sum
graded_monoid
graded_mul_action
hierarchy_design
indicator_function
invertible
is_prime_pow
linear_recurrence
modeq
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
elliptic_curve
point
weierstrass
locally_ringed_space
has_colimits
morphisms
basic
finite_type
open_immersion
quasi_compact
quasi_separated
ring_hom_properties
universally_closed
open_immersion
Scheme
basic
presheafed_space
gluing
has_colimits
prime_spectrum
basic
is_open_comap_C
maximal
noetherian
projective_spectrum
scheme
structure_sheaf
topology
AffineScheme
Gamma_Spec_adjunction
Scheme
Spec
function_field
gluing
limits
locally_ringed_space
presheafed_space
properties
pullbacks
ringed_space
sheafed_space
stalks
structure_sheaf
algebraic_topology
dold_kan
compatibility
decomposition
degeneracies
equivalence
equivalence_additive
equivalence_pseudoabelian
faces
functor_gamma
functor_n
gamma_comp_n
homotopies
homotopy_equivalence
n_comp_gamma
n_reflects_iso
normalized
notations
p_infty
projections
split_simplicial_object
fundamental_groupoid
basic
fundamental_group
induced_maps
product
punit
simply_connected
Moore_complex
alternating_face_map_complex
cech_nerve
extra_degeneracy
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
uniqueness
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
deriv
add
basic
comp
inv
inverse
linear
mul
polynomial
pow
prod
slope
star
support
zpow
fderiv
add
basic
bilinear
comp
equiv
linear
mul
prod
restrict_scalars
star
affine_map
bump_function_findim
bump_function_inner
cont_diff
cont_diff_def
darboux
diff_cont_on_cl
dslope
extend_deriv
fderiv_analytic
fderiv_measurable
fderiv_symmetric
formal_multilinear_series
implicit
inverse
iterated_deriv
lagrange_multipliers
lhopital
local_extr
mean_value
monotone
parametric_integral
parametric_interval_integral
series
tangent_cone
taylor
uniform_limits_deriv
complex
unit_disc
basic
upper_half_plane
basic
functions_bounded_at_infty
manifold
metric
topology
abs_max
arg
basic
cauchy_integral
circle
conformal
isometry
liouville
locally_uniform_limit
open_mapping
operator_norm
phragmen_lindelof
polynomial
re_im_topology
real_deriv
removable_singularity
schwarz
convex
cone
basic
dual
proper
simplicial_complex
basic
specific_functions
basic
deriv
basic
between
body
caratheodory
combination
complex
contractible
exposed
extrema
extreme
function
gauge
hull
independent
integral
intrinsic
jensen
join
krein_milman
measure
normed
partition_of_unity
proj_Icc
quasiconvex
segment
side
slope
star
stone_separation
strict
strict_convex_between
strict_convex_space
topology
uniform
fourier
add_circle
fourier_transform
poisson_summation
riemann_lebesgue_lemma
inner_product_space
adjoint
basic
calculus
conformal_linear_map
dual
euclidean_dist
gram_schmidt_ortho
l2_space
lax_milgram
linear_pmap
of_norm
orientation
orthogonal
pi_L2
positive
projection
rayleigh
spectrum
symmetric
two_dim
locally_convex
abs_convex
balanced_core_hull
basic
bounded
continuous_of_bounded
polar
strong_topology
weak_dual
with_seminorms
normed
field
basic
infinite_sum
unit_ball
group
SemiNormedGroup
completion
kernels
SemiNormedGroup
add_circle
add_torsor
ball_sphere
basic
completion
controlled_closure
hom
hom_completion
infinite_sum
pointwise
quotient
seminorm
order
basic
lattice
upper_lower
ring
seminorm
mul_action
normed_space
hahn_banach
extension
separation
star
basic
continuous_functional_calculus
exponential
gelfand_duality
matrix
mul
multiplier
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
continuous_linear_map
dual
dual_number
enorm
exponential
extend
extr
finite_dimension
indicator_function
int
is_R_or_C
linear_isometry
lp_equiv
lp_space
matrix_exponential
mazur_ulam
multilinear
operator_norm
pi_Lp
pointwise
quaternion_exponential
ray
riesz_lemma
spectrum
triv_sq_zero_ext
units
weak_dual
special_functions
complex
arg
circle
log
log_deriv
gamma
basic
beta
bohr_mollerup
log
base
basic
deriv
monotone
pow
asymptotics
complex
continuity
deriv
nnreal
real
trigonometric
angle
arctan
arctan_deriv
basic
bounds
chebyshev
complex
complex_deriv
deriv
euler_sine_prod
inverse
inverse_deriv
series
arsinh
bernstein
compare_exp
exp
exp_deriv
exponential
gaussian
improper_integrals
integrals
japanese_bracket
non_integrable
polar_coord
polynomials
sqrt
stirling
specific_limits
basic
floor_pow
normed
von_neumann_algebra
basic
bounded_variation
constant_speed
convolution
hofer
matrix
mean_inequalities
mean_inequalities_pow
mellin_transform
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
injective_resolution
left_derived
non_preadditive
opposite
projective
pseudoelements
right_derived
subobject
transfer
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
galois_connection
pairwise
preorder
ulift
closed
cartesian
functor
functor_category
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
groupoid
basic
free_groupoid
subgroupoid
vertex_group
idempotents
basic
biproducts
functor_categories
functor_extension
homological_complex
karoubi
karoubi_karoubi
simplicial_object
lifting_properties
adjunction
basic
limits
constructions
over
basic
connected
products
binary_products
epi_mono
equalizers
filtered
finite_products_of_binary_products
limits_of_products_and_equalizers
pullbacks
weakly_initial
zero_objects
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
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
filtered_colimit_commutes_finite_limit
final
fubini
full_subcategory
functor_category
has_limits
is_limit
kan_extension
lattice
mono_coprod
opposites
over
pi
presheaf
small_complete
types
unit
yoneda
linear
basic
functor_category
linear_functor
yoneda
localization
construction
opposite
predicate
monad
adjunction
algebra
basic
coequalizer
equiv_mon
kleisli
limits
monadicity
products
types
monoidal
free
basic
coherence
internal
Module
functor_category
limits
types
of_chosen_finite_products
basic
symmetric
rigid
basic
functor_category
of_equivalence
types
basic
coyoneda
symmetric
Bimod
CommMon_
End
Mod_
Mon_
braided
category
center
coherence
coherence_lemmas
discrete
functor
functor_category
functorial
limits
linear
natural_transformation
of_has_finite_products
opposite
preadditive
skeleton
subcategory
tor
transport
pi
basic
preadditive
yoneda
basic
injective
limits
projective
Mat
additive_functor
basic
biproducts
eilenberg_moore
endo_functor
functor_category
generator
hom_orthogonal
injective
injective_resolution
left_exact
of_biproducts
opposite
projective
projective_resolution
schur
single_obj
products
associator
basic
bifunctor
shift
basic
sigma
basic
sites
adjunction
canonical
closed
compatible_plus
compatible_sheafification
cover_lifting
cover_preserving
dense_subsite
grothendieck
induced_topology
left_exact
limits
plus
pretopology
pushforward
sheaf
sheaf_of_types
sheafification
sieves
spaces
subsheaf
surjective
types
whiskering
subobject
basic
comma
factor_thru
lattice
limits
mono_over
types
well_powered
sums
associator
basic
triangulated
basic
pretriangulated
rotate
triangulated
Fintype
action
adhesive
arrow
balanced
cofiltered_system
comm_sq
comma
conj
connected_components
core
differential_object
discrete_category
elements
elementwise
endomorphism
epi_mono
eq_to_hom
equivalence
essential_image
essentially_small
extensive
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
simple
single_obj
skeletal
structured_arrow
subterminal
thin
types
whiskering
with_terminal
yoneda
combinatorics
additive
behrend
e_transform
energy
pluennecke_ruzsa
ruzsa_covering
salem_spencer
derangements
basic
exponential
finite
hall
basic
finite
quiver
arborescence
basic
cast
connected_component
covering
path
push
single_obj
subquiver
symmetric
set_family
compression
down
uv
ahlswede_zhang
harris_kleitman
intersecting
kleitman
lym
shadow
simple_graph
ends
defs
properties
regularity
bound
chunk
energy
equitabilise
increment
lemma
uniform
triangle
basic
acyclic
adj_matrix
basic
clique
coloring
connectivity
degree_sum
density
finsubgraph
hasse
inc_matrix
matching
metric
partition
prod
strongly_regular
subgraph
trails
young
semistandard_tableau
young_diagram
catalan
colex
composition
configuration
double_counting
hales_jewett
hindman
partition
pigeonhole
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
count
set
buffer
parser
basic
numeral
basic
complex
basic
cardinality
determinant
exponential
exponential_bounds
module
orientation
countable
basic
defs
small
dfinsupp
basic
interval
lex
multiset
ne_locus
order
well_founded
dlist
basic
instances
enat
basic
lattice
fin
tuple
basic
bubble_sort_induction
monotone
nat_antidiagonal
reflection
sort
basic
fin2
interval
succ_pred
vec_notation
finite
basic
card
defs
set
finset
basic
card
fin
finsupp
fold
functor
image
interval
lattice
locally_finite
mul_antidiagonal
n_ary
nat_antidiagonal
noncomm_prod
option
order
pairwise
pi
pi_induction
pimage
pointwise
powerset
preimage
prod
sigma
slice
sort
sum
sups
sym
finsupp
alist
antidiagonal
basic
big_operators
defs
fin
fintype
indicator
interval
lex
multiset
ne_locus
order
pointwise
pwo
to_dfinsupp
well_founded
fintype
array
basic
big_operators
card
card_embedding
fin
lattice
list
option
order
parity
perm
pi
powerset
prod
quotient
sigma
small
sort
sum
units
vector
fp
basic
fun_like
basic
embedding
equiv
fintype
int
cast
basic
defs
field
lemmas
prod
dvd
basic
pow
order
basic
lemmas
units
absolute_value
associated
basic
bitwise
char_zero
conditionally_complete_order
div
gcd
interval
least_greatest
lemmas
log
modeq
nat_prime
parity
range
sqrt
succ_pred
units
is_R_or_C
basic
lemmas
lazy_list
basic
list
big_operators
basic
lemmas
alist
basic
chain
count
cycle
dedup
defs
destutter
duplicate
fin_range
forall2
func
indexes
infix
intervals
join
lattice
lemmas
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
to_finsupp
zip
matrix
auto
basic
basis
block
char_p
dmatrix
dual_number
hadamard
invertible
kronecker
notation
pequiv
rank
reflection
multiset
antidiagonal
basic
bind
dedup
finset_ops
fintype
fold
functor
interval
lattice
locally_finite
nat_antidiagonal
nodup
pi
powerset
range
sections
sort
sum
mv_polynomial
basic
cardinal
comap
comm_ring
counit
derivation
division
equiv
expand
funext
invertible
monad
pderiv
polynomial
rename
supported
variables
nat
cast
basic
defs
field
prod
with_top
choose
basic
bounds
cast
central
dvd
factorization
multinomial
sum
vandermonde
factorial
basic
big_operators
cast
double_factorial
factorization
basic
prime_pow
gcd
basic
big_operators
order
basic
lemmas
basic
bits
bitwise
count
digits
dist
even_odd_rec
factors
fib
hyperoperation
interval
lattice
log
modeq
multiplicity
nth
pairing
parity
part_enat
periodic
pow
prime
prime_fin
prime_norm_num
psub
set
size
sqrt
sqrt_norm_num
squarefree
succ_pred
totient
units
upto
with_bot
num
basic
bitwise
lemmas
prime
option
basic
defs
n_ary
ordmap
ordnode
ordset
pfunctor
multivariate
M
W
basic
univariate
M
basic
pi
algebra
interval
lex
pnat
basic
defs
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
partial_fractions
reverse
ring_division
splits
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
big_operators
cast
defs
denumerable
encodable
floor
init
lemmas
meta_defs
nnrat
order
sqrt
star
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
enat_ennreal
ennreal
ereal
golden_ratio
hyperreal
irrational
nnreal
pointwise
sign
sqrt
seq
computation
parallel
seq
wseq
set
intervals
basic
disjoint
group
infinite
instances
iso_Ioo
monoid
monotone
ord_connected
ord_connected_component
order_iso
pi
proj_Icc
surj_on
unordered_interval
with_bot_top
pairwise
basic
lattice
pointwise
basic
big_operators
finite
interval
iterate
list_of_fn
smul
support
Union_lift
accumulate
basic
bool_indicator
constructions
countable
enumerate
equitable
finite
function
functor
image
lattice
list
mul_antidiagonal
n_ary
ncard
opposite
prod
semiring
sigma
sups
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
add_circle
conservative
ergodic
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
spectrum
minpoly
basic
field
is_integrally_closed
splitting_field
construction
is_splitting_field
abel_ruffini
adjoin
ax_grothendieck
cardinality
chevalley_warning
finiteness
fixed
galois
intermediate_field
krull_topology
laurent
mv_polynomial
normal
perfect_closure
polynomial_galois_group
primitive_element
ratfunc
separable
separable_degree
subfield
tower
geometry
euclidean
angle
oriented
affine
basic
right_angle
rotation
unoriented
affine
basic
conformal
right_angle
sphere
sphere
basic
power
ptolemy
second_inter
basic
circumcenter
inversion
monge_point
triangle
manifold
algebra
left_invariant_derivation
lie_group
monoid
smooth_functions
structures
instances
real
sphere
units_of_normed_algebra
sheaf
basic
vector_bundle
basic
fiberwise_linear
hom
pullback
smooth_section
tangent
bump_function
charted_space
complex
conformal_groupoid
cont_mdiff
cont_mdiff_map
cont_mdiff_mfderiv
derivation_bundle
diffeomorph
local_invariant_properties
metrizable
mfderiv
partition_of_unity
smooth_manifold_with_corners
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
support
units
perm
cycle
basic
concrete
type
basic
fin
list
option
sign
subgroup
support
via_embedding
specific_groups
alternating
cyclic
dihedral
quaternion
subgroup
actions
basic
finite
mul_opposite
pointwise
saturated
simple
zpowers
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
matrix
midpoint
midpoint_zero
ordered
pointwise
restrict
slope
basis
bilinear
bilinear_form
tensor_product
charpoly
basic
to_matrix
clifford_algebra
basic
conjugation
contraction
equivs
even
even_equiv
fold
grading
star
direct_sum
finsupp
tensor_product
eigenspace
basic
is_alg_closed
minpoly
exterior_algebra
basic
grading
of_alternating
free_module
finite
basic
matrix
rank
basic
determinant
ideal_quotient
norm
pid
rank
strong_rank_condition
matrix
charpoly
basic
coeff
eigs
finite_field
linear_map
minpoly
absolute_value
adjugate
basis
bilinear_form
block
circulant
determinant
diagonal
dot_product
dual
finite_dimensional
general_linear_group
hermitian
invariant_basis_number
is_diag
ldl
mv_polynomial
nondegenerate
nonsingular_inverse
orthogonal
polynomial
pos_def
reindex
schur_complement
sesquilinear_form
special_linear_group
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
dual
isometry
prod
real
tensor_algebra
basic
grading
to_tensor_power
tensor_product
matrix
adic_completion
alternating
annihilating_polynomial
basic
basis
bilinear_form
bilinear_map
coevaluation
contraction
cross_product
determinant
dfinsupp
dimension
dual
finite_dimensional
finrank
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
quotient_pi
ray
sesquilinear_form
smodeq
span
std_basis
symplectic_group
tensor_power
tensor_product
tensor_product_basis
trace
unitary_group
vandermonde
logic
embedding
basic
set
encodable
basic
lattice
equiv
array
basic
defs
embedding
fin
fintype
functor
list
local_equiv
nat
option
set
transfer_instance
function
basic
conjugate
iterate
small
basic
list
basic
denumerable
hydra
is_empty
lemmas
nonempty
nontrivial
pairwise
relation
relator
unique
measure_theory
category
Meas
constructions
borel_space
basic
complex
continuous_linear_map
metrizable
prod
basic
integral
pi
polish
covering
besicovitch
besicovitch_vector_space
density_theorem
differentiation
liminf_limsup
one_dim
vitali
vitali_family
decomposition
jordan
lebesgue
radon_nikodym
signed_hahn
unsigned_hahn
function
conditional_expectation
ae_measurable
basic
condexp_L1
condexp_L2
indicator
real
unique
special_functions
arctan
basic
inner
is_R_or_C
strongly_measurable
basic
inner
lp
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_seminorm
lp_space
simple_func
simple_func_dense
simple_func_dense_lp
uniform_integrable
group
action
add_circle
arithmetic
fundamental_domain
geometry_of_numbers
integration
measurable_equiv
measure
pointwise
prod
integral
average
bochner
circle_integral
circle_transform
divergence_theorem
exp_decay
fund_thm_calculus
integrable_on
integral_eq_improper
interval_average
interval_integral
layercake
lebesgue
lebesgue_normed_space
mean_inequalities
peak_function
periodic
riesz_markov_kakutani
set_integral
set_to_l1
torus_integral
vitali_caratheodory
measure
haar
basic
inner_product_space
normed_space
of_basis
quotient
lebesgue
basic
complex
eq_haar
integral
ae_disjoint
ae_measurable
complex
content
doubling
finite_measure
giry_monad
hausdorff
measure_space
measure_space_def
mutually_singular
null_measurable
open_pos
outer_measure
portmanteau
probability_measure
regular
stieltjes
sub
vector_measure
with_density_vector_measure
order
upper_lower
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
cyclotomic
basic
discriminant
gal
primitive_roots
rat
legendre_symbol
quadratic_char
basic
gauss_sum
add_character
basic
gauss_eisenstein_lemmas
gauss_sum
jacobi_symbol
mul_character
norm_num
quadratic_reciprocity
zmod_char
liouville
basic
liouville_number
liouville_with
measure
residual
modular_forms
jacobi_theta
basic
manifold
basic
congruence_subgroups
slash_actions
slash_invariant_forms
number_field
basic
canonical_embedding
class_number
embeddings
norm
units
padics
hensel
padic_integers
padic_norm
padic_numbers
padic_val
ring_homs
zsqrtd
basic
gaussian_int
quadratic_reciprocity
to_real
ADE_inequality
arithmetic_function
basic
bernoulli
bernoulli_polynomials
bertrand
dioph
diophantine_approximation
divisors
fermat4
fermat_psp
frobenius_number
function_field
kummer_dedekind
l_series
lucas_lehmer
lucas_primality
modular
multiplicity
pell
pell_matiyasevic
prime_counting
primes_congruent_one
primorial
pythagorean_triples
ramification_inertia
sum_four_squares
sum_two_squares
von_mangoldt
well_approximable
wilson
zeta_function
zeta_values
order
atoms
finite
bounds
basic
order_iso
category
BddDistLat
BddLat
BddOrd
BoolAlg
CompleteLat
DistLat
FinBddDistLat
FinBoolAlg
FinPartOrd
Frm
HeytAlg
Lat
LinOrd
NonemptyFinLinOrd
PartOrd
Preord
Semilat
omega_complete_partial_order
conditionally_complete_lattice
basic
finset
group
extension
linear
well
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
hom
regular
hom
basic
bounded
complete_lattice
lattice
order
set
monotone
basic
extension
monovary
odd
union
partition
equipartition
finpartition
rel_iso
basic
group
set
succ_pred
basic
interval_succ
limit
linear_locally_finite
relation
upper_lower
basic
hom
locally_finite
antichain
antisymmetrization
atoms
basic
boolean_algebra
bounded
bounded_order
chain
circular
closure
compactly_generated
compare
complete_boolean_algebra
complete_lattice
complete_lattice_intervals
concept
copy
countable_dense_linear_order
cover
directed
disjoint
disjointed
fixed_points
galois_connection
game_add
grade
height
ideal
initial_seg
interval
irreducible
iterate
jordan_holder
lattice
lattice_intervals
liminf_limsup
locally_finite
max
min_max
minimal
modular_lattice
omega_complete_partial_order
ord_continuous
order_iso_nat
partial_sups
pfilter
prime_ideal
prop_instances
rel_classes
semiconj_Sup
sup_indep
symm_diff
synonym
well_founded
well_founded_set
with_bot
zorn
zorn_atoms
probability
independence
basic
zero_one
kernel
basic
composition
cond_cdf
cond_distrib
condexp
disintegration
integral_comp_prod
invariance
measurable_integral
with_density
martingale
basic
borel_cantelli
centering
convergence
optional_sampling
optional_stopping
upcrossing
probability_mass_function
basic
constructions
monad
uniform
process
adapted
filtration
hitting_time
stopping
borel_cantelli
cond_count
conditional_expectation
conditional_probability
density
ident_distrib
integration
moments
notation
strong_law
variance
representation_theory
group_cohomology
basic
resolution
Action
Rep
basic
character
fdRep
invariants
maschke
ring_theory
adjoin
basic
fg
field
power_basis
tower
coprime
basic
ideal
lemmas
dedekind_domain
S_integer
adic_valuation
basic
dvr
factorization
finite_adele_ring
ideal
integral_closure
pid
selmer_group
derivation
basic
lie
to_square_zero
discrete_valuation_ring
basic
tfae
graded_algebra
basic
homogeneous_ideal
homogeneous_localization
radical
ideal
associated_prime
basic
cotangent
idempotent_fg
local_ring
minimal_prime
norm
operations
over
prod
quotient
quotient_operations
int
basic
localization
away
adjoin_root
basic
as_subring
at_prime
basic
cardinality
fraction_ring
ideal
integer
integral
inv_submonoid
localization_localization
module
norm
num_denom
submodule
mv_polynomial
basic
homogeneous
ideal
symmetric
tower
weighted_homogeneous
non_unital_subsemiring
basic
ore_localization
basic
ore_set
polynomial
cyclotomic
basic
eval
expand
roots
eisenstein
basic
is_integral
hermite
basic
gaussian
basic
bernstein
chebyshev
content
dickson
gauss_lemma
opposites
pochhammer
quotient
rational_root
scale_roots
selmer
tower
vieta
power_series
basic
well_known
ring_hom
finite
finite_type
integral
surjective
roots_of_unity
basic
complex
minpoly
subring
basic
pointwise
subsemiring
basic
pointwise
valuation
basic
extend_to_localization
integers
integral
quotient
ramification_group
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
complex
congruence
discriminant
eisenstein_criterion
etale
euclidean_domain
filtration
finite_presentation
finite_type
finiteness
fintype
flat
fractional_ideal
free_comm_ring
free_ring
hahn_series
henselian
integral_closure
integral_domain
integrally_closed
is_adjoin_root
is_tensor_product
jacobson
jacobson_ideal
kaehler
laurent_series
local_properties
matrix_algebra
multiplicity
nakayama
nilpotent
noetherian
non_zero_divisors
norm
nullstellensatz
perfection
polynomial_algebra
power_basis
prime
principal_ideal_domain
quotient_nilpotent
quotient_noetherian
rees_algebra
ring_hom_properties
ring_invo
simple_module
tensor_product
trace
unique_factorization_domain
zmod
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
exponential
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
assert_exists
auto_cases
binder_matching
by_contra
cache
cancel_denoms
chain
choose
clear
compute_degree
congr
congrm
core
dec_trivial
delta_instance
dependencies
derive_fintype
derive_inhabited
doc_commands
elementwise
elide
equiv_rw
expand_exists
explode
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
mk_simp_attribute
move_add
noncomm_ring
nontriviality
norm_cast
norm_fin
norm_num
norm_swap
observe
obviously
pi_instances
polyrith
positivity
pretty_cases
print_sorry
project_dir
protected
push_neg
qify
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
to_additive
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
group
basic
compact
infinite_sum
basic
module
order
real
ring
module
basic
character_space
determinant
finite_dimension
linear_pmap
locally_convex
multilinear
simple
star
strong_topology
weak_dual
nonarchimedean
adic_topology
bases
basic
order
archimedean
compact
extend_from
extr_closure
field
filter
floor
group
intermediate_value
left_right
left_right_lim
liminf_limsup
monotone_continuity
monotone_convergence
proj_Icc
t5
upper_lower
ring
basic
ideal
affine
algebra
const_mul_action
constructions
continuous_affine_map
continuous_monoid_hom
equicontinuity
field
filter_basis
group_completion
group_with_zero
localization
monoid
mul_action
open_subgroup
polynomial
semigroup
star
star_subalgebra
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
basic
projective
Profinite
as_limit
basic
cofiltered_limit
projective
Top
limits
basic
cofiltered
konig
products
pullbacks
adjunctions
basic
epi_mono
open_nhds
opens
Born
Compactum
Locale
TopCommRing
UniformSpace
continuous_function
algebra
basic
bounded
cocompact_map
compact
ideals
locally_constant
ordered
polynomial
stone_weierstrass
t0_sierpinski
units
weierstrass
zero_at_infty
fiber_bundle
basic
constructions
is_homeomorphic_trivial_bundle
trivialization
hom
open
homotopy
H_spaces
basic
contractible
equiv
homotopy_group
path
product
instances
add_circle
complex
discrete
ennreal
ereal
int
irrational
matrix
nat
nnreal
rat
rat_lemmas
real
real_vector_space
sign
triv_sq_zero_ext
locally_constant
algebra
basic
metric_space
algebra
antilipschitz
baire
basic
cantor_scheme
cau_seq_filter
closeds
completion
contracting
dilation
emetric_paracompact
emetric_space
equicontinuity
gluing
gromov_hausdorff
gromov_hausdorff_realized
hausdorff_dimension
hausdorff_distance
holder
infsep
isometric_smul
isometry
kuratowski
lipschitz
metric_separated
metrizable
metrizable_uniformity
partition_of_unity
pi_nat
polish
shrinking_lemma
thickened_indicator
order
hom
basic
esakia
basic
lattice
lower_topology
priestley
sets
closeds
compacts
opens
order
sheaves
sheaf_condition
equalizer_products
opens_le_cover
pairwise_intersections
sites
unique_gluing
abelian
forget
functors
limits
local_predicate
locally_surjective
operations
presheaf
presheaf_of_functions
punit
sheaf
sheaf_of_functions
sheafify
skyscraper
stalks
spectral
hom
uniform_space
absolute_value
abstract_completion
basic
cauchy
compact
compact_convergence
compare_reals
complete_separated
completion
equicontinuity
equiv
matrix
pi
separation
uniform_convergence
uniform_convergence_topology
uniform_embedding
vector_bundle
basic
constructions
hom
G_delta
alexandroff
bases
basic
compact_open
connected
constructions
continuous_on
covering
dense_embedding
discrete_quotient
extend_from
extremally_disconnected
filter
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
partial
partition_of_unity
path_connected
perfect
quasi_separated
semicontinuous
separation
sequences
shrinking_lemma
sober
stone_cech
subset_properties
support
tactic
tietze_extension
unit_interval
urysohns_bounded
urysohns_lemma
mathlib-archive
examples
mersenne_primes
prop_encodable
imo
imo1959_q1
imo1960_q1
imo1962_q1
imo1962_q4
imo1964_q1
imo1969_q1
imo1972_q5
imo1975_q1
imo1977_q6
imo1981_q3
imo1987_q1
imo1988_q6
imo1994_q1
imo1998_q2
imo2001_q2
imo2001_q6
imo2005_q3
imo2005_q4
imo2006_q3
imo2006_q5
imo2008_q2
imo2008_q3
imo2008_q4
imo2011_q3
imo2011_q5
imo2013_q1
imo2013_q5
imo2019_q1
imo2019_q2
imo2019_q4
imo2020_q2
imo2021_q1
miu_language
basic
decision_nec
decision_suf
oxford_invariants
2021summer
week3_p1
wiedijk_100_theorems
abel_ruffini
area_of_a_circle
ascending_descending_sequences
ballot_problem
birthday_problem
cubing_a_cube
friendship_graphs
herons_formula
inverse_triangle_sum
konigsberg
partition
perfect_numbers
solution_of_cubic
sum_of_prime_reciprocals_diverges
arithcc
sensitivity
mathlib-counterexamples
canonically_ordered_comm_semiring_two_mul
char_p_zero_ne_char_zero
cyclotomic_105
direct_sum_is_internal
girard
homogeneous_prime_not_prime
linear_order_with_pos_mul_pos_eq_zero
map_floor
phillips
pseudoelement
quadratic_form
seminorm_lattice_not_distrib
sorgenfrey_line
zero_divisors_in_add_monoid_algebras
Color scheme
dark
system
light