comp_tensorRId_eq — Mathlib

English

For a quadratic form Q1, composing with the right id-tensor yields the same as tensoring with the square map: Q1 ∘ (rid) = Q1 ⊗ sq.

Русский

Для квадратичной формы Q1 композиция с правым тензорным единичным отображением rid равна Q1 ⊗ sq.

LaTeX

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

Lean4

theorem comp_tensorRId_eq (Q₁ : QuadraticForm R M₁) : Q₁.comp (TensorProduct.rid R M₁) = Q₁.tmul (sq (R := R)) :=
  by
  refine (QuadraticMap.associated_rightInverse R).injective ?_
  ext m₁ m₁'
  dsimp [-associated_apply]
  simp only [associated_tmul, QuadraticMap.associated_comp]
  simp [-associated_apply, one_mul]

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