Powers_of_Ring_Elements
Provedproofwikiring-theory
In a ring, a^m * a^n = a^(m+n) for all natural numbers m, n.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Powers_of_Ring_Elements {R : Type _} [Ring R] (a : R) (m n : ℕ) : a ^ m * a ^ n = a ^ (m + n) := by sorrySource