OAI/Analysis/SymmetricDomains/EtaleDerivationExtensionUnique.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Release061.analyticCoordinateline 35 - theorem
OAI.Release061.analyticGerm_aevalline 38 - theorem
OAI.Release061.algebraicIndependent_analyticCoordinateline 52 - def
OAI.Release061.etaleDerivationExtensionline 76 - theorem
OAI.Release061.etaleDerivationExtension_algebraMapline 83 - theorem
OAI.Release061.etaleDerivationExtension_uniqueline 93