smul_mk — Mathlib

English

For a group action on V and a nonzero vector v, the action on the projectivization coincides with taking the class of g•v.

Русский

Для действия группы на V и ненулевого вектора v действие на проективном пространстве даёт тот же класс, что и образ g•v.

LaTeX

$$$ g \cdot \mathrm{mk}(K,v,hv) = \mathrm{mk}(K,g \cdot v, (smul\_ne\_zero\_iff\_ne g).mpr hv) $$$

Lean4

@[simp]
theorem smul_mk (g : G) {v : V} (hv : v ≠ 0) : g • mk K v hv = mk K (g • v) ((smul_ne_zero_iff_ne g).mpr hv) :=
  rfl

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