inl_inr — Mathlib

English

For any m1, m2, the pair (m1,0) and (0,m2) are orthogonal under the product form.

Русский

Для любых m1, m2 пара (m1,0) и (0,m2) ортогональны относительно произведения.

LaTeX

$$(Q1.prod Q2).IsOrtho (m1,0) (0,m2)$$

Lean4

@[simp]
theorem inl_inr {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ : M₁) (m₂ : M₂) :
    (Q₁.prod Q₂).IsOrtho (m₁, 0) (0, m₂) :=
  QuadraticMap.IsOrtho.prod (.zero_right _) (.zero_left _)

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