English
Let B1 be a bilinear form on M1 over A and B2 a bilinear form on M2 over R. Then the tensor product B1 ⊗ B2 defines a bilinear form on M1 ⊗ M2, and for simple tensors it satisfies (B1 ⊗ B2)(m1 ⊗ m2, m1' ⊗ m2') = B2(m2, m2') · B1(m1, m1').
Русский
Пусть B1 — билинейная форма на M1 над A и B2 — билинейная форма на M2 над R. Тогда тензорное произведение B1 ⊗ B2 определяет билинейную форму на M1 ⊗ M2, и на простых тензорах выполняется (B1 ⊗ B2)(m1 ⊗ m2, m1' ⊗ m2') = B2(m2, m2') · B1(m1, m1').
LaTeX
$$$$\tensorDistrib\;R\;A\; (B_1 \otimes_\mathrm{tmul} B_2)\; (m_1 \otimes m_2)\; (m_1' \otimes m_2') = B_2(m_2,m_2') \cdot B_1(m_1,m_1').$$$$
Lean4
@[simp]
theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) :
tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₂ m₂ m₂' • B₁ m₁ m₁' :=
rfl
