OAI/Analysis/CircleDomains/Transfer/ComplexC1LevelChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Regular scalar coordinates with both ambient spaces represented by ℂ.

  1. lemma OAI.CircleDomainRigidity.exists_complex_c1_level_chart line 11