English
There is an action of GL(2,K) on OnePoint(K) induced by the projectivization identification with the projective line.
Русский
Существует действие GL(2,K) на OnePoint(K), полученное через эквивалентность к проективной линии.
LaTeX
$$$\\text{GL}(2,K)\\curvearrowright \\mathrm{OnePoint}(K).$$$
Lean4
/-- For a field `K`, the group `GL(2, K)` acts on `OnePoint K`, via the canonical identification
with the `ℙ¹(K)` (which is given explicitly by Möbius transformations). -/
instance instGLAction : MulAction (GL (Fin 2) K) (OnePoint K) :=
(equivProjectivization K).mulAction (GL (Fin 2) K)