OAI/Geometry/TamingCompatibility/Hodge/HodgeSmoothPatch.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.TamingCompatibility.HodgeChart.rawVector_fun_smulline 17 - lemma
OAI.TamingCompatibility.HodgeChart.manifoldTest_eqline 23 - def
OAI.TamingCompatibility.GeometricHilbert.hodgeMultiplyline 50 - lemma
OAI.TamingCompatibility.GeometricHilbert.hodge_exists_patchline 55 - lemma
OAI.TamingCompatibility.GeometricHilbert.hodge_supported_testline 74 - lemma
OAI.TamingCompatibility.GeometricHilbert.hodge_local_pairing_eqline 128