isOrtho_inl_inl_iff — Mathlib

English

Let Q1 and Q2 be quadratic maps as above. Then the product map is orthogonal on pairs that live entirely in the left component, i.e. (m1,0) and (m1',0) are orthogonal iff Q1 is orthogonal on (m1,m1').

Русский

Пусть Q1 и Q2 — квадратичные отображения. Тогда ортогональность пары (m1,0), (m1',0) для произведения эквивалентна ортогональности m1, m1' для Q1.

LaTeX

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

Lean4

@[simp]
theorem isOrtho_inl_inl_iff {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ m₁' : M₁) :
    (Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁' := by simp [isOrtho_def]

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