mathlib3 documentation

tactic.noncomm_ring

source
meta def tactic.interactive.noncomm_ring  :
tactic unit

A tactic for simplifying identities in not-necessarily-commutative rings.

An example:

example {R : Type*} [ring R] (a b c : R) : a * (b + c + c - b) = 2*a*c :=
by noncomm_ring
source
def tactic_doc.tactic.noncomm_ring  :
tactic_doc_entry

A tactic for simplifying identities in not-necessarily-commutative rings.

An example:

example {R : Type*} [ring R] (a b c : R) : a * (b + c + c - b) = 2*a*c :=
by noncomm_ring