tmul_tensorLId_apply — Mathlib

English

The map tensorLId Q2 is the same as TensorProduct.lid on the level of linear maps.

Русский

То же отражение для tensorLId, т.е. она совпадает с TensorProduct.lid на уровне линейных отображений.

LaTeX

$$$tensorLId\, Q_2 = \, \mathrm{TensorProduct}.lid\, R\, M_2$$$

Lean4

@[simp]
theorem tmul_tensorLId_apply (Q₂ : QuadraticForm R M₂) (x : R ⊗[R] M₂) :
    Q₂ (TensorProduct.lid R M₂ x) = QuadraticForm.tmul (sq (R := R)) Q₂ x :=
  DFunLike.congr_fun (comp_tensorLId_eq Q₂) x

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