tensorDistrib_tmul — Mathlib

English

For Q1, Q2, M1, M2, the tensorDistrib_tmul identity expresses that the action on a pure tensor is the product of the actions on each factor.

Русский

ТензорDistrib_tmul на чистом тензоре равен произведению действий на каждую фигуру.

LaTeX

$$$\\text{tensorDistrib}_R^A (Q_1 \\otimes_\\text{tmul} Q_2) (m_1 \\otimes_\\text{tmul} m_2) = Q_1(m_1) \\otimes_\\! Q_2(m_2)$$$

Lean4

@[simp]
theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) :
    tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ :=
  letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
  (LinearMap.BilinForm.tensorDistrib_tmul _ _ _ _ _ _ _ _).trans <|
    congr_arg₂ _ (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)

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