mul_zpow — Mathlib

English

If A and B commute, then for every integer i, (A B)^i = A^i B^i.

Русский

Если A и B commuting, то для любого целого i выполняется (AB)^i = A^i B^i.

LaTeX

$$$ \text{Commute}(A,B) \Rightarrow \forall i \in \mathbb{Z},\ (A B)^i = A^i B^i $$$

Lean4

theorem mul_zpow {A B : M} (h : Commute A B) : ∀ i : ℤ, (A * B) ^ i = A ^ i * B ^ i
  | (n : ℕ) => by simp [h.mul_pow n]
  | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev, h.mul_pow n.succ, (h.pow_pow _ _).eq]

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