tensorRId — Mathlib

English

For a quadratic form Q1, composing with rid is equivalent to tensoring with sq: Q1 ∘ rid = Q1 ⊗ sq.

Русский

Связь rid и sq: Q1 ∘ rid = Q1 ⊗ sq.

LaTeX

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

Lean4

/-- `TensorProduct.rid` preserves tensor products of quadratic forms. -/
@[simps toLinearEquiv]
def tensorRId (Q₁ : QuadraticForm R M₁) : (Q₁.tmul (sq (R := R))).IsometryEquiv Q₁
    where
  toLinearEquiv := TensorProduct.rid R M₁
  map_app' := tmul_tensorRId_apply Q₁

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