The noncomm_ring tactic #
Solve goals in not necessarily commutative rings.
This tactic is rudimentary, but useful for solving simple goals in noncommutative rings. One
glaring flaw is that numeric powers are unfolded entirely with pow_succ and can easily exceed the
maximum recursion depth.
noncomm_ring is just a simp only [some lemmas] followed by abel. It automatically uses abel1
to close the goal, and if that doesn't succeed, defaults to abel_nf.
theorem
Mathlib.Tactic.NoncommRing.nat_lit_mul_eq_nsmul
{R : Type u_1}
[NonAssocSemiring R]
(r : R)
(n : ℕ)
[Nat.AtLeastTwo n]
:
OfNat.ofNat n * r = n • r
theorem
Mathlib.Tactic.NoncommRing.mul_nat_lit_eq_nsmul
{R : Type u_1}
[NonAssocSemiring R]
(r : R)
(n : ℕ)
[Nat.AtLeastTwo n]
:
r * OfNat.ofNat n = n • r
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
Equations
- Mathlib.Tactic.NoncommRing.noncomm_ring = Lean.ParserDescr.node `Mathlib.Tactic.NoncommRing.noncomm_ring 1024 (Lean.ParserDescr.nonReservedSymbol "noncomm_ring" false)