tmul_zero

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#TensorProduct.tmul_zero

English

A pure tensor with a zero factor is zero: for any m ∈ M, 0 ⊗ n = 0 and m ⊗ 0 = 0.

Русский

Чистый тензор с нулевым фактором равен нулю: 0 ⊗ n = 0 и m ⊗ 0 = 0.

LaTeX

$$$ (0 \\otimes_R n) = 0, \\quad (m \\otimes_R 0) = 0. $$$

Lean4

@[simp]
theorem tmul_zero (m : M) : m ⊗ₜ[R] (0 : N) = 0 :=
  Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero_right _

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

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

Разделы

Аффилиация

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