Index

A

abel	apply, [1] assumption

B

by_contra

C

calc cases change check command open commands check

commutative ring congr constructor continuity contrapose convert

D

definitional equality differential calculus

divisibility dsimp

E

elementary calculus exact, [1]

exponential ext extensionality

F

field_simp

Filter from

G

gcd goal

group (algebraic structure) (tactic)

H

have, [1]

I

implicit argument inequalities

integration, [1] intro

L

lambda abstraction lcm left

linarith linear map local context logarithm

M

matrices max measure theory

metric space min monoid monotone function

N

namespace

norm_num normed space

O

open

P

proof state

push_neg

R

rcases real numbers reflexivity rewrite

rfl right ring (algebraic structure), [1] rintro rw, [1]

S

set operations

simp

T

tactics abel apply, [1] assumption by_contra and by_contradiction calc cases change congr constructor continuity contrapose convert dsimp exact, [1] ext field_simp from group have, [1] intro left linarith norm_num push_neg rcases refl and reflexivity right rintro rw and rewrite, [1] simp use

this topological space topology

U

use

V

vector space

vector subspace