one_mul

Mathlib.RingTheory.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.one_mul

English

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

Русский

Степень k простого тензора распадается как произведение степеней: (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

protected theorem one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x := by
  refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru