exists_smul_eq_mk_rep — Mathlib

English

There exists a unit a ∈ Kˣ such that a·v equals the representative of its projective point, i.e. a·v = (mk K v hv).rep.

Русский

Существует единичный элемент a ∈ Kˣ такой, что a·v является представителем соответствующей точки проективного пространства: a·v = (mk K v hv).rep.

LaTeX

$$$ \exists a \in K^\times,\ a \cdot v = (\mathrm{mk}\ K\ v\ hv).\mathrm{rep} $$$

Lean4

theorem exists_smul_eq_mk_rep (v : V) (hv : v ≠ 0) : ∃ a : Kˣ, a • v = (mk K v hv).rep :=
  (mk_eq_mk_iff K _ _ (rep_nonzero _) hv).1 (mk_rep _)

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