smul_infty_def — Mathlib

English

The action of g on ∞ is the image under the equivalence of the projectivization of the column vector (g00, g10), i.e. [g00:g10].

Русский

Действие g на ∞ равно образу в проективном пространстве вектора-столбца (g00,g10), т.е. [g00:g10].

LaTeX

$$$g\\cdot \\infty = (\\equivProjectivization(K)).\\mathrm{symm}(\\mathrm{mk}K(g_{00},g_{10})\\,\\text{with det nonzero})$$$

Lean4

theorem smul_infty_def {g : GL (Fin 2) K} :
    g • ∞ =
      (equivProjectivization K).symm
        (.mk K (g 0 0, g 1 0) (fun h ↦ by simpa [det_fin_two, Prod.mk_eq_zero.mp h] using g.det_ne_zero)) :=
  by simp [Equiv.smul_def, mulVec_eq_sum, Units.smul_def]

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