mathlib documentation

tactic.​ring

tactic.​ring

source
conv.​interactive.​ring
tactic.​interactive.​ring
tactic.​interactive.​ring.​mode
tactic.​interactive.​ring1
tactic.​ring.​add_atom
tactic.​ring.​add_neg_eq_sub
tactic.​ring.​cache
tactic.​ring.​cache.​cs_app
tactic.​ring.​const_add_horner
tactic.​ring.​eval
tactic.​ring.​eval'
tactic.​ring.​eval_add
tactic.​ring.​eval_atom
tactic.​ring.​eval_const_mul
tactic.​ring.​eval_horner
tactic.​ring.​eval_mul
tactic.​ring.​eval_neg
tactic.​ring.​eval_pow
tactic.​ring.​get_atom
tactic.​ring.​get_cache
tactic.​ring.​has_coe
tactic.​ring.​has_coe_to_fun
tactic.​ring.​has_to_tactic_format
tactic.​ring.​horner
tactic.​ring.​horner_add_const
tactic.​ring.​horner_add_horner_eq
tactic.​ring.​horner_add_horner_gt
tactic.​ring.​horner_add_horner_lt
tactic.​ring.​horner_atom
tactic.​ring.​horner_const_mul
tactic.​ring.​horner_def'
tactic.​ring.​horner_expr
tactic.​ring.​horner_expr.​e
tactic.​ring.​horner_expr.​is_zero
tactic.​ring.​horner_expr.​pp
tactic.​ring.​horner_expr.​refl_conv
tactic.​ring.​horner_expr.​to_string
tactic.​ring.​horner_expr.​xadd'
tactic.​ring.​horner_horner
tactic.​ring.​horner_mul_const
tactic.​ring.​horner_mul_horner
tactic.​ring.​horner_mul_horner_zero
tactic.​ring.​horner_neg
tactic.​ring.​horner_pow
tactic.​ring.​ic_lift
tactic.​ring.​ic_lift'
tactic.​ring.​inhabited
tactic.​ring.​lift
tactic.​ring.​mul_assoc_rev
tactic.​ring.​nc_lift
tactic.​ring.​normalize
tactic.​ring.​normalize_mode
tactic.​ring.​normalize_mode.​has_reflect
tactic.​ring.​pow_add_rev
tactic.​ring.​pow_add_rev_right
tactic.​ring.​pow_succ
tactic.​ring.​ring_m
tactic.​ring.​ring_m.​alternative
tactic.​ring.​ring_m.​monad
tactic.​ring.​ring_m.​run
tactic.​ring.​subst_into_pow
tactic.​ring.​unfold_div
tactic.​ring.​unfold_sub
tactic.​ring.​zero_horner

ring

Evaluate expressions in the language of commutative (semi)rings. Based on http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf .

source
def tactic.​ring.​horner {α : Type u_1} [comm_semiring α] :
α → α → ℕ → α → α

The normal form that ring uses is mediated by the function horner a x n b := a * x ^ n + b. The reason we use a definition rather than the (more readable) expression on the right is because this expression contains a number of typeclass arguments in different positions, while horner contains only one comm_semiring instance at the top level. See also horner_expr for a description of normal form.

Equations
source
meta structure tactic.​ring.​cache  :
Type

This cache contains data required by the ring tactic during execution.

source
@[instance]
meta def tactic.​ring.​ring_m.​monad  :
monad tactic.ring.ring_m

source
meta def tactic.​ring.​ring_m  :
Type → Type

The monad that ring works in. This is a reader monad containing a mutable cache (using ref for mutability), as well as the list of atoms-up-to-defeq encountered thus far, used for atom sorting.

source
@[instance]
meta def tactic.​ring.​ring_m.​alternative  :
alternative tactic.ring.ring_m

source
meta def tactic.​ring.​get_cache  :
tactic.ring.ring_m tactic.ring.cache

Get the ring data from the monad.

source
meta def tactic.​ring.​get_atom  :
ℕ → tactic.ring.ring_m expr

Get an already encountered atom by its index.

source
meta def tactic.​ring.​add_atom  :
expr → tactic.ring.ring_m ℕ

Get the index corresponding to an atomic expression, if it has already been encountered, or put it in the list of atoms and return the new index, otherwise.

source
meta def tactic.​ring.​lift {α : Type} :
tactic α → tactic.ring.ring_m α

Lift a tactic into the ring_m monad.

source
meta def tactic.​ring.​ring_m.​run (red : tactic.transparency) (e : expr) {α : Type} :
tactic.ring.ring_m α → tactic α

Run a ring_m tactic in the tactic monad.

source
meta def tactic.​ring.​ic_lift' (icf : tactic.ring.cache → tactic.ref tactic.instance_cache) {α : Type} :
(tactic.instance_cache → tactic (tactic.instance_cache × α)) → tactic.ring.ring_m α

Lift an instance cache tactic (probably from norm_num) to the ring_m monad. This version is abstract over the instance cache in question (either the ring α, or ℕ for exponents).

source
meta def tactic.​ring.​ic_lift {α : Type} :
(tactic.instance_cache → tactic (tactic.instance_cache × α)) → tactic.ring.ring_m α

Lift an instance cache tactic (probably from norm_num) to the ring_m monad. This uses the instance cache corresponding to the ring α.

source
meta def tactic.​ring.​nc_lift {α : Type} :
(tactic.instance_cache → tactic (tactic.instance_cache × α)) → tactic.ring.ring_m α

Lift an instance cache tactic (probably from norm_num) to the ring_m monad. This uses the instance cache corresponding to ℕ, which is used for computations in the exponent.

source
meta def tactic.​ring.​cache.​cs_app  :
tactic.ring.cache → name → list expr → expr

Apply a theorem that expects a comm_semiring instance. This is a special case of ic_lift mk_app, but it comes up often because horner and all its theorems have this assumption; it also does not require the tactic monad which improves access speed a bit.

source
meta inductive tactic.​ring.​horner_expr  :
Type

Every expression in the language of commutative semirings can be viewed as a sum of monomials, where each monomial is a product of powers of atoms. We fix a global order on atoms (up to definitional equality), and then separate the terms according to their smallest atom. So the top level expression is a * x^n + b where x is the smallest atom and n > 0 is a numeral, and n is maximal (so a contains at least one monomial not containing an x), and b contains no monomials with an x (hence all atoms in b are larger than x).

If there is no x satisfying these constraints, then the expression must be a numeral. Even though we are working over rings, we allow rational constants when these can be interpreted in the ring, so we can solve problems like x / 3 = 1 / 3 * x even though these are not technically in the language of rings.

These constraints ensure that there is a unique normal form for each ring expression, and so the algorithm is simply to calculate the normal form of each side and compare for equality.

To allow us to efficiently pattern match on normal forms, we maintain this inductive type that holds a normalized expression together with its structure. All the exprs in this type could be removed without loss of information, and conversely the horner_expr structure and the ℕ and ℚ values can be recovered from the top level expr, but we keep both in order to keep proof producing normalization functions efficient.

source
meta def tactic.​ring.​horner_expr.​e  :
tactic.ring.horner_expr → expr

Get the expression corresponding to a horner_expr. This can be calculated recursively from the structure, but we cache the exprs in all subterms so that this function can be computed in constant time.

source
meta def tactic.​ring.​horner_expr.​is_zero  :
tactic.ring.horner_expr → bool

Is this expr the constant 0?

source
@[instance]
meta def tactic.​ring.​has_coe  :
has_coe tactic.ring.horner_expr expr

source
@[instance]
meta def tactic.​ring.​has_coe_to_fun  :
has_coe_to_fun tactic.ring.horner_expr

source
meta def tactic.​ring.​horner_expr.​xadd'  :
tactic.ring.cache → tactic.ring.horner_expr → expr × ℕ → expr × ℕ → tactic.ring.horner_expr → tactic.ring.horner_expr

Construct a xadd node, generating the cached expr using the input cache.

source
meta def tactic.​ring.​horner_expr.​to_string  :
tactic.ring.horner_expr → string

Pretty printer for horner_expr.

source
meta def tactic.​ring.​horner_expr.​pp  :
tactic.ring.horner_expr → tactic format

Pretty printer for horner_expr.

source
@[instance]
meta def tactic.​ring.​has_to_tactic_format  :
has_to_tactic_format tactic.ring.horner_expr

source
meta def tactic.​ring.​horner_expr.​refl_conv  :
tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Reflexivity conversion for a horner_expr.

source
theorem tactic.​ring.​zero_horner {α : Type u_1} [comm_semiring α] (x : α) (n : ℕ) (b : α) :
tactic.ring.horner 0 x n b = b

source
theorem tactic.​ring.​horner_horner {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ n₂ : ℕ) (b : α) (n' : ℕ) :
n₁ + n₂ = n' → tactic.ring.horner (tactic.ring.horner a₁ x n₁ 0) x n₂ b = tactic.ring.horner a₁ x n' b

source
meta def tactic.​ring.​eval_horner  :
tactic.ring.horner_expr → expr × ℕ → expr × ℕ → tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate horner a n x b where a and b are already in normal form.

source
theorem tactic.​ring.​const_add_horner {α : Type u_1} [comm_semiring α] (k a x : α) (n : ℕ) (b b' : α) :
k + b = b' → k + tactic.ring.horner a x n b = tactic.ring.horner a x n b'

source
theorem tactic.​ring.​horner_add_const {α : Type u_1} [comm_semiring α] (a x : α) (n : ℕ) (b k b' : α) :
b + k = b' → tactic.ring.horner a x n b + k = tactic.ring.horner a x n b'

source
theorem tactic.​ring.​horner_add_horner_lt {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (b₂ : α) (k : ℕ) (a' b' : α) :
n₁ + k = n₂ → a₁ + tactic.ring.horner a₂ x k 0 = a' → b₁ + b₂ = b' → tactic.ring.horner a₁ x n₁ b₁ + tactic.ring.horner a₂ x n₂ b₂ = tactic.ring.horner a' x n₁ b'

source
theorem tactic.​ring.​horner_add_horner_gt {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (b₂ : α) (k : ℕ) (a' b' : α) :
n₂ + k = n₁ → tactic.ring.horner a₁ x k 0 + a₂ = a' → b₁ + b₂ = b' → tactic.ring.horner a₁ x n₁ b₁ + tactic.ring.horner a₂ x n₂ b₂ = tactic.ring.horner a' x n₂ b'

source
theorem tactic.​ring.​horner_add_horner_eq {α : Type u_1} [comm_semiring α] (a₁ x : α) (n : ℕ) (b₁ a₂ b₂ a' b' t : α) :
a₁ + a₂ = a' → b₁ + b₂ = b' → tactic.ring.horner a' x n b' = t → tactic.ring.horner a₁ x n b₁ + tactic.ring.horner a₂ x n b₂ = t

source
meta def tactic.​ring.​eval_add  :
tactic.ring.horner_expr → tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a + b where a and b are already in normal form.

source
theorem tactic.​ring.​horner_neg {α : Type u_1} [comm_ring α] (a x : α) (n : ℕ) (b a' b' : α) :
-a = a' → -b = b' → -tactic.ring.horner a x n b = tactic.ring.horner a' x n b'

source
meta def tactic.​ring.​eval_neg  :
tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate -a where a is already in normal form.

source
theorem tactic.​ring.​horner_const_mul {α : Type u_1} [comm_semiring α] (c a x : α) (n : ℕ) (b a' b' : α) :
c * a = a' → c * b = b' → c * tactic.ring.horner a x n b = tactic.ring.horner a' x n b'

source
theorem tactic.​ring.​horner_mul_const {α : Type u_1} [comm_semiring α] (a x : α) (n : ℕ) (b c a' b' : α) :
a * c = a' → b * c = b' → tactic.ring.horner a x n b * c = tactic.ring.horner a' x n b'

source
meta def tactic.​ring.​eval_const_mul  :
expr × ℚ → tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate k * a where k is a rational numeral and a is in normal form.

source
theorem tactic.​ring.​horner_mul_horner_zero {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (aa t : α) :
tactic.ring.horner a₁ x n₁ b₁ * a₂ = aa → tactic.ring.horner aa x n₂ 0 = t → tactic.ring.horner a₁ x n₁ b₁ * tactic.ring.horner a₂ x n₂ 0 = t

source
theorem tactic.​ring.​horner_mul_horner {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (b₂ aa haa ab bb t : α) :
tactic.ring.horner a₁ x n₁ b₁ * a₂ = aa → tactic.ring.horner aa x n₂ 0 = haa → a₁ * b₂ = ab → b₁ * b₂ = bb → haa + tactic.ring.horner ab x n₁ bb = t → tactic.ring.horner a₁ x n₁ b₁ * tactic.ring.horner a₂ x n₂ b₂ = t

source
meta def tactic.​ring.​eval_mul  :
tactic.ring.horner_expr → tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a * b where a and b are in normal form.

source
theorem tactic.​ring.​horner_pow {α : Type u_1} [comm_semiring α] (a x : α) (n m n' : ℕ) (a' : α) :
n * m = n' → a ^ m = a' → tactic.ring.horner a x n 0 ^ m = tactic.ring.horner a' x n' 0

source
theorem tactic.​ring.​pow_succ {α : Type u_1} [comm_semiring α] (a : α) (n : ℕ) (b c : α) :
a ^ n = b → b * a = c → a ^ (n + 1) = c

source
meta def tactic.​ring.​eval_pow  :
tactic.ring.horner_expr → expr × ℕ → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a ^ n where a is in normal form and n is a natural numeral.

source
theorem tactic.​ring.​horner_atom {α : Type u_1} [comm_semiring α] (x : α) :
x = tactic.ring.horner 1 x 1 0

source
meta def tactic.​ring.​eval_atom  :
expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a where a is an atom.

source
theorem tactic.​ring.​subst_into_pow {α : Type u_1} [monoid α] (l : α) (r : ℕ) (tl : α) (tr : ℕ) (t : α) :
l = tl → r = tr → tl ^ tr = t → l ^ r = t

source
theorem tactic.​ring.​unfold_sub {α : Type u_1} [add_group α] (a b c : α) :
a + -b = c → a - b = c

source
theorem tactic.​ring.​unfold_div {α : Type u_1} [division_ring α] (a b c : α) :
a * b⁻¹ = c → a / b = c

source
meta def tactic.​ring.​eval  :
expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a ring expression e recursively to normal form, together with a proof of equality.

source
meta def tactic.​ring.​eval'  :
tactic.transparency → expr → tactic (expr × expr)

Evaluate a ring expression e recursively to normal form, together with a proof of equality.

source
theorem tactic.​ring.​horner_def' {α : Type u_1} [comm_semiring α] (a x : α) (n : ℕ) (b : α) :
tactic.ring.horner a x n b = x ^ n * a + b

source
theorem tactic.​ring.​mul_assoc_rev {α : Type u_1} [semigroup α] (a b c : α) :
a * (b * c) = a * b * c

source
theorem tactic.​ring.​pow_add_rev {α : Type u_1} [monoid α] (a : α) (m n : ℕ) :
a ^ m * a ^ n = a ^ (m + n)

source
theorem tactic.​ring.​pow_add_rev_right {α : Type u_1} [monoid α] (a b : α) (m n : ℕ) :
b * a ^ m * a ^ n = b * a ^ (m + n)

source
theorem tactic.​ring.​add_neg_eq_sub {α : Type u_1} [add_group α] (a b : α) :
a + -b = a - b

source
@[instance]
meta def tactic.​ring.​normalize_mode.​has_reflect  :
has_reflect tactic.ring.normalize_mode

source
inductive tactic.​ring.​normalize_mode  :
Type

If ring fails to close the goal, it falls back on normalizing the expression to a "pretty" form so that you can see why it failed. This setting adjusts the resulting form:

  • raw is the form that ring actually uses internally, with iterated applications of horner. Not very readable but useful if you don't want any postprocessing. This results in terms like horner (horner (horner 3 y 1 0) x 2 1) x 1 (horner 1 y 1 0).
  • horner maintains the Horner form structure, but it unfolds the horner definition itself, and tries to otherwise minimize parentheses. This results in terms like (3 * x ^ 2 * y + 1) * x + y.
  • SOP means sum of products form, expanding everything to monomials. This results in terms like 3 * x ^ 3 * y + x + y.
source
@[instance]
def tactic.​ring.​inhabited  :
inhabited tactic.ring.normalize_mode

Equations
source
meta def tactic.​ring.​normalize  :
tactic.transparency → (tactic.ring.normalize_mode := tactic.ring.normalize_mode.horner) → expr → tactic (expr × expr)

A ring-based normalization simplifier that rewrites ring expressions into the specified mode.

  • raw is the form that ring actually uses internally, with iterated applications of horner. Not very readable but useful if you don't want any postprocessing. This results in terms like horner (horner (horner 3 y 1 0) x 2 1) x 1 (horner 1 y 1 0).
  • horner maintains the Horner form structure, but it unfolds the horner definition itself, and tries to otherwise minimize parentheses. This results in terms like (3 * x ^ 2 * y + 1) * x + y.
  • SOP means sum of products form, expanding everything to monomials. This results in terms like 3 * x ^ 3 * y + x + y.
source
meta def tactic.​interactive.​ring1  :
interactive.parse (optional (lean.parser.tk "!")) → tactic unit

Tactic for solving equations in the language of commutative (semi)rings. This version of ring fails if the target is not an equality that is provable by the axioms of commutative (semi)rings.

source
meta def tactic.​interactive.​ring.​mode  :
lean.parser tactic.ring.normalize_mode

Parser for ring's mode argument, which can only be the "keywords" raw, horner or SOP. (Because these are not actually keywords we use a name parser and postprocess the result.)

source
meta def tactic.​interactive.​ring  :
interactive.parse (optional (lean.parser.tk "!")) → interactive.parse tactic.interactive.ring.mode → interactive.parse interactive.types.location → tactic unit

Tactic for solving equations in the language of commutative (semi)rings. Attempts to prove the goal outright if there is no at specifier and the target is an equality, but if this fails it falls back to rewriting all ring expressions into a normal form. When writing a normal form, ring SOP will use sum-of-products form instead of horner form. ring! will use a more aggressive reducibility setting to identify atoms.

Based on Proving Equalities in a Commutative Ring Done Right in Coq by Benjamin Grégoire and Assia Mahboubi.

source
meta def conv.​interactive.​ring  :
interactive.parse (optional (lean.parser.tk "!")) → interactive.parse tactic.interactive.ring.mode → conv unit

Normalises expressions in commutative (semi-)rings inside of a conv block using the tactic ring.

General documentation

index
tactics
commands
hole commands
attributes
notes

Additional documentation

mathlib overview
tactic writing
calc mode
conv mode
simplification
well founded recursion
style guide
documentation style guide
naming conventions

Library

algebra
big_operators
basic
intervals
order
pi
ring
category
Algebra
basic
limits
CommRing
adjunctions
basic
colimits
limits
Group
Z_Module_equivalence
abelian
adjunctions
basic
biproducts
colimits
images
limits
preadditive
zero
Module
abelian
basic
kernels
limits
monoidal
Mon
basic
colimits
limits
continued_fractions
computation
approximations
basic
correctness_terminating
translations
basic
continuants_recurrence
convergents_equiv
terminated_stable
translations
group
basic
commute
conj
defs
hom
inj_surj
pi
prod
semiconj
to_additive
type_tags
ulift
units
units_hom
with_one
homology
chain_complex
exact
homology
image_to_kernel_map
module
basic
ordered
pi
prod
submodule
ulift
polynomial
big_operators
ring
basic
pi
prod
ulift
add_torsor
archimedean
associated
char_p
char_zero
classical_lie_algebras
direct_limit
direct_sum
divisibility
euclidean_domain
field
field_power
floor
free
free_monoid
gcd_monoid
geom_sum
group_action_hom
group_power
group_ring_action
group_with_zero
group_with_zero_power
invertible
iterate_hom
lie_algebra
linear_ordered_comm_group_with_zero
linear_recurrence
midpoint
opposites
order
order_functions
ordered_field
ordered_group
ordered_ring
pointwise
punit_instances
quadratic_discriminant
algebraic_geometry
presheafed_space
prime_spectrum
stalks
analysis
ODE
gronwall
analytic
basic
composition
calculus
darboux
deriv
extend_deriv
fderiv
implicit
inverse
iterated_deriv
lhopital
local_extr
mean_value
specific_functions
tangent_cone
times_cont_diff
complex
basic
polynomial
convex
basic
caratheodory
cone
extrema
specific_functions
topology
normed_space
add_torsor
banach
basic
bounded_linear_maps
complemented
dual
enorm
extend
finite_dimension
hahn_banach
indicator_function
mazur_ulam
multilinear
operator_norm
point_reflection
real_inner_product
riesz_lemma
units
special_functions
arsinh
exp_log
pow
trigonometric
asymptotics
hofer
mean_inequalities
specific_limits
category_theory
abelian
diagram_lemmas
four
basic
exact
non_preadditive
pseudoelements
adjunction
basic
fully_faithful
limits
opposites
category
Cat
Groupoid
Kleisli
Rel
default
closed
cartesian
monoidal
concrete_category
basic
bundled
bundled_hom
reflects_isomorphisms
unbundled_hom
limits
preserves
basic
shapes
shapes
constructions
over
connected
default
products
binary_products
equalizers
limits_of_products_and_equalizers
preserve_binary_products
pullbacks
binary_products
biproducts
concrete_category
equalizers
finite_limits
finite_products
images
kernels
products
pullbacks
regular_mono
strong_epi
terminal
types
wide_pullbacks
zero
concrete_category
cones
connected
creates
fubini
functor_category
lattice
limits
opposites
over
pi
punit
types
monad
adjunction
algebra
basic
bundled
equiv_mon
limits
types
monoidal
internal
functor_category
types
End
braided
category
functor
functor_category
functorial
internal
of_has_finite_products
types
unitors
pi
basic
preadditive
biproducts
default
schur
products
associator
basic
bifunctor
sums
associator
basic
action
arrow
comma
conj
connected
const
core
currying
differential_object
discrete_category
elements
endomorphism
epi_mono
eq_to_hom
equivalence
full_subcategory
fully_faithful
functor
functor_category
functorial
graded_object
groupoid
hom_functor
isomorphism
isomorphism_classes
natural_isomorphism
natural_transformation
opposites
over
pempty
punit
quotient
reflects_isomorphisms
shift
simple
single_obj
sparse
types
whiskering
yoneda
combinatorics
composition
simple_graph
computability
halting
partrec
partrec_code
primrec
reduce
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
fold
functor
uliftable
core
data
buffer
parser
bitvec
buffer
dlist
lazy_list
stream
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
rbmap
basic
rbtree
basic
default
sigma
basic
lex
string
basic
ops
subtype
basic
instances
sum
basic
unsigned
basic
ops
prod
punit
quot
repr
set
setoid
to_string
meta
converter
conv
interactive
lean
parser
smt
congruence_closure
ematch
interactive
rsimp
smt_tactic
widget
basic
html_cmd
interactive_expr
replace_save_info
tactic_component
ac_tactics
async_tactic
attribute
backward
case_tag
comp_value_tactics
congr_lemma
congr_tactic
constructor_tactic
contradiction_tactic
declaration
derive
environment
exceptional
expr
expr_address
float
format
fun_info
has_reflect
hole_command
injection_tactic
interaction_monad
interactive
interactive_base
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
data
analysis
filter
topology
array
lemmas
bitvec
basic
buffer
basic
complex
basic
exponential
module
dlist
basic
instances
equiv
encodable
basic
lattice
basic
denumerable
fin
functor
list
local_equiv
mul_add
nat
ring
transfer_instance
finset
basic
fold
intervals
lattice
nat_antidiagonal
order
pi
powerset
sort
finsupp
basic
lattice
pointwise
fintype
basic
card
intervals
sort
fp
basic
int
basic
cast
char_zero
gcd
modeq
parity
range
sqrt
list
alist
bag_inter
basic
chain
defs
erase_dup
forall2
func
indexes
intervals
min_max
nat_antidiagonal
nodup
of_fn
pairwise
palindrome
perm
range
rotate
sections
sigma
sort
tfae
zip
matrix
basic
notation
pequiv
multiset
antidiagonal
basic
erase_dup
finset_ops
fold
functor
intervals
lattice
nat_antidiagonal
nodup
pi
powerset
range
sections
sort
nat
basic
cast
choose
digits
dist
enat
fib
gcd
modeq
multiplicity
pairing
parity
prime
sqrt
totient
num
basic
bitwise
lemmas
prime
option
basic
defs
padics
hensel
padic_integers
padic_norm
padic_numbers
pfunctor
multivariate
M
W
basic
univariate
M
basic
pnat
basic
factors
intervals
xgcd
polynomial
degree
basic
algebra_map
basic
coeff
degree
derivative
div
eval
field_division
identities
induction
integral_normalization
monic
monomial
ring_division
qpf
multivariate
constructions
cofix
comp
const
fix
prj
quot
sigma
basic
univariate
basic
rat
basic
cast
denumerable
floor
meta_defs
order
sqrt
real
basic
cardinality
cau_seq
cau_seq_completion
conjugate_exponents
ennreal
ereal
golden_ratio
hyperreal
irrational
nnreal
pi
seq
computation
parallel
seq
wseq
set
intervals
basic
disjoint
image_preimage
ord_connected
unordered_interval
basic
countable
disjointed
enumerate
finite
function
lattice
setoid
basic
partition
sigma
basic
stream
basic
string
basic
defs
zmod
basic
zsqrtd
basic
gaussian_int
W
bool
char
dfinsupp
erased
fin
fin2
fin_enum
finmap
hash_map
holor
indicator_function
lazy_list2
mllist
monoid_algebra
mv_polynomial
opposite
pequiv
pfun
prod
quot
rel
semiquot
subtype
sum
support
sym
sym2
tree
typevec
ulift
vector2
deprecated
group
ring
subgroup
submonoid
dynamics
circle
rotation_number
translation_number
fixed_points
basic
topology
periodic_pts
field_theory
algebraic_closure
chevalley_warning
finite
fixed
minimal_polynomial
mv_polynomial
normal
perfect_closure
separable
splitting_field
subfield
tower
geometry
algebra
lie_group
euclidean
basic
circumcenter
monge_point
triangle
manifold
basic_smooth_bundle
charted_space
local_invariant_properties
mfderiv
real_instances
smooth_manifold_with_corners
times_cont_mdiff
group_theory
perm
cycles
sign
submonoid
basic
membership
operations
abelianization
congruence
coset
eckmann_hilton
free_abelian_group
free_group
group_action
monoid_localization
order_of_element
presented_group
quotient_group
semidirect_product
subgroup
sylow
linear_algebra
affine_space
basic
combination
finite_dimensional
independent
char_poly
coeff
direct_sum
finsupp
tensor_product
adic_completion
basic
basis
bilinear_form
char_poly
contraction
determinant
dimension
direct_sum_module
dual
finite_dimensional
finsupp
finsupp_vector_space
invariant_basis_number
lagrange
linear_action
linear_pmap
matrix
multilinear
nonsingular_inverse
projection
quadratic_form
sesquilinear_form
smodeq
special_linear_group
tensor_algebra
tensor_product
logic
function
basic
conjugate
iterate
basic
embedding
nontrivial
relation
relator
unique
measure_theory
category
Meas
ae_eq_fun
bochner_integration
borel_space
content
decomposition
giry_monad
group
haar_measure
integration
interval_integral
l1_space
lebesgue_measure
measurable_space
measure_space
outer_measure
probability_mass_function
set_integral
simple_func_dense
meta
coinductive_predicates
expr
expr_lens
rb_map
uchange
number_theory
basic
bernoulli
dioph
lucas_lehmer
pell
primorial
pythagorean_triples
quadratic_reciprocity
sum_four_squares
sum_two_squares
order
category
LinearOrder
NonemptyFinLinOrd
PartialOrder
Preorder
filter
at_top_bot
bases
basic
cofinite
countable_Inter
extr
filter_product
germ
indicator_function
interval
lift
partial
pointwise
ultrafilter
basic
boolean_algebra
bounded_lattice
bounds
complete_boolean_algebra
complete_lattice
conditionally_complete_lattice
copy
directed
fixed_points
galois_connection
ideal
iterate
lattice
lexicographic
liminf_limsup
ord_continuous
order_iso_nat
pilex
rel_classes
rel_iso
semiconj_Sup
zorn
representation_theory
maschke
ring_theory
ideal
basic
operations
over
polynomial
basic
homogeneous
rational_root
valuation
basic
adjoin
adjoin_root
algebra
algebra_operations
algebra_tower
algebraic
coprime
derivation
discrete_valuation_ring
eisenstein_criterion
euclidean_domain
fintype
fractional_ideal
free_comm_ring
free_ring
integral_closure
integral_domain
jacobson
jacobson_ideal
localization
maps
matrix_algebra
multiplicity
noetherian
polynomial_algebra
power_series
prime
principal_ideal_domain
subring
subsemiring
tensor_product
unique_factorization_domain
set_theory
game
domineering
impartial
nim
short
state
winner
cardinal
cardinal_ordinal
cofinality
game
lists
ordinal
ordinal_arithmetic
ordinal_notation
pgame
schroeder_bernstein
surreal
zfc
system
random
basic
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
abel
algebra
alias
apply
apply_fun
auto_cases
binder_matching
cache
cancel_denoms
chain
choose
clear
core
dec_trivial
delta_instance
derive_fintype
derive_inhabited
doc_commands
elide
equiv_rw
explode
ext
fin_cases
find
find_unused
finish
fix_reflect_string
generalize_proofs
generalizes
group
hint
interactive
interactive_expr
interval_cases
lift
local_cache
localized
mk_iff_of_inductive_prop
noncomm_ring
norm_cast
norm_num
obviously
pi_instances
protected
push_neg
rcases
reassoc_axiom
rename_var
replacer
restate_axiom
rewrite
ring
ring2
ring_exp
scc
show_term
simp_command
simp_result
simp_rw
simpa
simps
slice
solve_by_elim
split_ifs
squeeze
subtype_instance
suggest
tauto
tfae
tidy
transfer
transform_decl
transport
trunc_cases
unfold_cases
where
with_local_reducibility
wlog
zify
topology
algebra
affine
continuous_functions
group
group_completion
infinite_sum
module
monoid
multilinear
open_subgroup
ordered
polynomial
ring
uniform_group
uniform_ring
category
Top
adjunctions
basic
epi_mono
limits
open_nhds
opens
TopCommRing
UniformSpace
instances
complex
ennreal
nnreal
real
real_vector_space
metric_space
antilipschitz
baire
basic
cau_seq_filter
closeds
completion
contracting
emetric_space
gluing
gromov_hausdorff
gromov_hausdorff_realized
hausdorff_distance
isometry
lipschitz
pi_Lp
premetric_space
sheaves
presheaf
presheaf_of_functions
sheaf
sheaf_of_functions
stalks
uniform_space
absolute_value
abstract_completion
basic
cauchy
compact_separated
compare_reals
complete_separated
completion
pi
separation
uniform_convergence
uniform_embedding
bases
basic
bounded_continuous_function
compact_open
compacts
constructions
continuous_map
continuous_on
dense_embedding
extend_from_subset
homeomorph
list
local_extr
local_homeomorph
maps
opens
order
path_connected
separation
sequences
stone_cech
subset_properties
tactic
topological_fiber_bundle