Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4

Fubin Yan, Kenneth W. Shum

The extended complex plane is a fundamental object in complex analysis, hyperbolic geometry, and mathematical physics. Its geometry is governed by Möbius transformations, with the…