Möbius transformations

Stream: Is there code for X?

[Jireh Loreaux]

I see we have https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.html for the upper half plane, but do we have anything for Möbius transformations on ℂ? Of course, I could ask the same for the Riemann sphere, but I don't know that we have anything for OnePoint ℂ anyway.

[Thomas Waring]

There is docs#OnePoint.instGLAction — which is the action of the general linear group on the one-point compactification of a field via Möebius transformations as shown in docs#OnePoint.smul_some_eq_ite

[Antoine Chambert-Loir]

As I said in Maxim's PR, a great bunch of what is in ## Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction would work for GL(2,K) acting on K by homographies.

[Antoine Chambert-Loir]

This is not an actual action, of course, but docs#Projectivization.instMulAction shows that GL(V) acts on docs#Projectivization