inr_inl — Mathlib

English

Let Q1 and Q2 be quadratic maps on M1 and M2 with values in P. Then for every m1 in M1 and m2 in M2, the pair (0, m2) and (m1, 0) are orthogonal with respect to the product map Q1.prod Q2.

Русский

Пусть Q1 и Q2 — квадратичные отображения на M1 и M2 в P. Тогда для любых m1 ∈ M1 и m2 ∈ M2 пары (0, m2) и (m1, 0) ортогональны относительно произведения {Q1.prod Q2}.

LaTeX

$$$ (Q_1 \\text{ prod } Q_2).\\mathrm{IsOrtho}((0,m_2),(m_1,0)). $$$

Lean4

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

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