zpow_add — Mathlib

English

Let a be an element of a group G. For all integers m,n, a^(m+n) = a^m a^n.

Русский

Пусть a принадлежит группе G. Для всех целых m,n выполняется a^(m+n) = a^m a^n.

LaTeX

$$$\forall a \in G,\ \forall m,n \in \mathbb{Z},\ a^{m+n} = a^{m} a^{n}$$$

Lean4

@[to_additive add_zsmul]
theorem zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
  induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]

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