tmul_pow — Mathlib

English

The k-th hpow of a simple tensor distributes: (a ⊗ b)^{k} = a^{k} ⊗ b^{k}.

Русский

k-я степень hpow простого тензора распределяется: (a ⊗ b)^k = a^k ⊗ b^k.

LaTeX

$$$ (a \otimes_R b)^k = a^k \otimes_R b^k \quad (k \in \mathbb{N}) $$$

Lean4

@[simp]
theorem tmul_pow (a : A) (b : B) (k : ℕ) : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k) := by
  induction k with
  | zero => simp [one_def]
  | succ k ih => simp [pow_succ, ih]

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