mathlib
documentation
data
.
rat
.
default
Google site search
data
.
rat
.
default
source
Imports
init.default
data.rat.floor
Imported by
Default Imports to Work With Rational Numbers
#
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
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
support
to_direct_sum
order
hom
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
field_power
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
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
complex
upper_half_plane
basic
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
normed_space
hahn_banach
extension
separation
star
basic
complex
exponential
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
exp
exp_deriv
exponential
gamma
gaussian
integrals
non_integrable
polar_coord
polynomials
pow
pow_deriv
sqrt
specific_limits
basic
floor_pow
normed
von_neumann_algebra
basic
convolution
fourier
hofer
matrix
mean_inequalities
mean_inequalities_pow
p_series
quaternion
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
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
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
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
sum
vandermonde
factorial
basic
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
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
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
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_integral_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
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
mul_character
quadratic_char
quadratic_reciprocity
zmod_char
liouville
basic
liouville_constant
liouville_with
measure
residual
modular_forms
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
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
ennreal
extr
filter_product
germ
indicator_function
interval
lift
modeq
n_ary
partial
pi
pointwise
prod
small_sets
ultrafilter
heyting
basic
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
imp
initial_seg
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
convergence
upcrossing
probability_mass_function
basic
constructions
monad
uniform
cond_count
conditional_expectation
conditional_probability
density
hitting_time
ident_distrib
independence
integration
moments
notation
stopping
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
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
lemmas
nth_rewrite
basic
congr
default
omega
int
dnf
form
main
preterm
nat
dnf
form
main
neg_elim
preterm
sub_elim
clause
coeffs
eq_elim
find_ees
find_scalars
lin_comb
main
misc
prove_unsats
term
rewrite_all
basic
rewrite_search
discovery
explain
frontend
search
types
abel
algebra
alias
apply
apply_fun
auto_cases
binder_matching
by_contra
cache
cancel_denoms
chain
choose
clear
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
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_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_convergence
compact_separated
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