# 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
```