prod — Mathlib

English

Pairwise orthogonality transfers to the product form.

Русский

Параллельная ортогональность переносится в форму произведения.

LaTeX

$$If Q1.IsOrtho v1 w1 and Q2.IsOrtho v2 w2 then (Q1.prod Q2).IsOrtho (v,w)$$

Lean4

theorem prod {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {v w : M₁ × M₂} (h₁ : Q₁.IsOrtho v.1 w.1)
    (h₂ : Q₂.IsOrtho v.2 w.2) : (Q₁.prod Q₂).IsOrtho v w :=
  (congr_arg₂ HAdd.hAdd h₁ h₂).trans <| add_add_add_comm _ _ _ _

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