OAI/Analysis/SymmetricDomains/LocalRealHomExtension.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Release061.local_real_hom_nat_mulline 34 - theorem
OAI.Release061.local_real_hom_subdivision_independentline 59 - theorem
OAI.Release061.local_real_hom_extensionline 79