orthogonal_mk — Mathlib

English

For nonzero representatives v and w, the projective orthogonality of mk F v hv and mk F w hw is equivalent to v ⬝ᵥ w = 0.

Русский

Для ненулевых представлений v и w ортогональность mk F v hv и mk F w hw эквивалентна v ⬝ᵥ w = 0.

LaTeX

$$$\\operatorname{orthogonal}(\\operatorname{mk}(F,v,hv),\\operatorname{mk}(F,w,hw)) \\iff v \\;\\!\\cdot\\!\\; w = 0$$$

Lean4

theorem orthogonal_mk {v w : m → F} (hv : v ≠ 0) (hw : w ≠ 0) : orthogonal (mk F v hv) (mk F w hw) ↔ v ⬝ᵥ w = 0 :=
  Iff.rfl

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