def ring : Lean.ParserDescr

Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent. If the goal is not appropriate for ring (e.g. not an equality) ring_nf will be suggested.

• ring! will use a more aggressive reducibility setting to determine equality of atoms.
• ring1 fails if the target is not an equality.

For example:

example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf

Equations

• ring = Lean.ParserDescr.node `ring 1024 (Lean.ParserDescr.nonReservedSymbol "ring" false)

def ring_at : Lean.ParserDescr

Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent. If the goal is not appropriate for ring (e.g. not an equality) ring_nf will be suggested.

• ring! will use a more aggressive reducibility setting to determine equality of atoms.
• ring1 fails if the target is not an equality.

For example:

example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf

Equations

• One or more equations did not get rendered due to their size.

def exists_delab' : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for existential quantifier, including extended binders.

Equations

• One or more equations did not get rendered due to their size.

theorem pow_self_ne_zero (n : ℕ) : n ^ n ≠ 0