OAI/Analysis/CircleDomains/Selection/PrincipalMobiusIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A principally normalized Möbius transformation is the identity. The finite-coordinate remainder is entire and tends to zero at infinity.

  1. theorem OAI.CircleDomainRigidity.principal_mobius_identity line 13