Mathlib.Tactic.NoncommRing

Module docstring

{"# 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. "}

Mathlib.Tactic.NoncommRing.nat_lit_mul_eq_nsmul theorem

[n.AtLeastTwo] : ofNat(n) * r = OfNat.ofNat n • r

Full source

lemma nat_lit_mul_eq_nsmul [n.AtLeastTwo] : ofNat(n) * r = OfNat.ofNat n • r := by
  simp only [nsmul_eq_mul, Nat.cast_ofNat]

Numeral Multiplication Equals Scalar Multiplication: $n \cdot r = n \bullet r$

Informal description

For any natural number $n \geq 2$ and any element $r$ in a ring $R$, the product of the numeral $n$ and $r$ is equal to the $n$-th multiple of $r$ under scalar multiplication, i.e., $n \cdot r = n \bullet r$.

Mathlib.Tactic.NoncommRing.mul_nat_lit_eq_nsmul theorem

[n.AtLeastTwo] : r * ofNat(n) = OfNat.ofNat n • r

Full source

lemma mul_nat_lit_eq_nsmul [n.AtLeastTwo] : r * ofNat(n) = OfNat.ofNat n • r := by
  simp only [nsmul_eq_mul', Nat.cast_ofNat]

Right Multiplication by Natural Number Equals Scalar Multiplication: $r * n = n \cdot r$

Informal description

For any element $r$ in a ring $R$ and any natural number $n \geq 2$, the product $r * n$ equals the scalar multiplication of $r$ by $n$, i.e., $r * n = n \cdot r$.

Mathlib.Tactic.NoncommRing.noncomm_ring definition

: Lean.ParserDescr✝

Full source

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

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

You can use `noncomm_ring [h]` to also simplify using `h`.
-/
syntax (name := noncomm_ring) "noncomm_ring" optConfig (discharger)?
  (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic

Noncommutative ring simplification tactic

Informal description

A tactic for simplifying identities in not-necessarily-commutative rings. It works by applying a set of simplification lemmas followed by the `abel` tactic. The tactic automatically attempts to close the goal using `abel1`, and if that fails, it falls back to `abel_nf`. Example usage: For elements $a, b, c$ in a ring $R$, the tactic can simplify $a * (b + c + c - b)$ to $2 * a * c$.