isOrtho_inr_inr_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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