tmul_tensorRId_apply — Mathlib

English

For a quadratic form Q1 and x in M1 ⊗ R, Q1(TensorProduct.rid x) equals Q1 ⊗ sq applied to x.

Русский

Для квадратичной формы Q1 и x в M1 ⊗ R, Q1( TensorProduct.rid x ) равно Q1 ⊗ sq, применённому к x.

LaTeX

$$$Q_1( \mathrm{TensorProduct}.rid\,R\,M_1\,x ) = Q_1 \otimes \mathrm{sq}(R := R)\,x$$$

Lean4

@[simp]
theorem tmul_tensorRId_apply (Q₁ : QuadraticForm R M₁) (x : M₁ ⊗[R] R) :
    Q₁ (TensorProduct.rid R M₁ x) = Q₁.tmul (sq (R := R)) x :=
  DFunLike.congr_fun (comp_tensorRId_eq Q₁) x

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