mul_pow — Mathlib

English

For any a in a monoid and any m,n ∈ ℕ, a^m and a^n commute.

Русский

Для любого a в моноиде и любых m,n ∈ ℕ, a^m и a^n коммутируют.

LaTeX

$$$\\forall M [Monoid M],\\ {a \\in M},\\ \forall m,n \\in\\mathbb{N},\\ Commute (a^m) (a^n)$$$

Lean4

@[to_additive]
theorem mul_pow (h : Commute a b) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
  | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
  | n + 1 => by simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]

Похожие утверждения