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 : ) [n.AtLeastTwo] :
OfNat.ofNat n * r = n r
theorem Mathlib.Tactic.NoncommRing.mul_nat_lit_eq_nsmul {R : Type u_1} [NonAssocSemiring R] (r : R) (n : ) [n.AtLeastTwo] :
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

You can use noncomm_ring [h] to also simplify using h.

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