mk_eq_mk_iff — Mathlib

English

For nonzero v,w ∈ V, the two projective points mk_K v hv and mk_K w hw are equal if and only if there exists a unit a ∈ Kˣ with a • w = v.

Русский

Для ненулевых векторов v, w ∈ V соответствующие проективные точки [v] и [w] совпадают тогда и только тогда, когда существует автономный скаляр a ∈ Kˣ such that v = a·w.

LaTeX

$$$ mk\ K\ v\ hv = mk\ K\ w\ hw \iff \exists a : K^\times, a \cdot w = v $$$

Lean4

theorem mk_eq_mk_iff (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w hw ↔ ∃ a : Kˣ, a • w = v :=
  Quotient.eq''

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