OAI/Geometry/TamingCompatibility/DifferentialForms/FormEquiv.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TamingCompatibility.MetricHodge.formEquivline 30 - lemma
OAI.TamingCompatibility.MetricHodge.formEquiv_applyline 34 - lemma
OAI.TamingCompatibility.MetricHodge.formEquiv_symm_applyline 37 - lemma
OAI.TamingCompatibility.MetricHodge.volumeSquare_compline 42 - def
OAI.TamingCompatibility.MetricHodge.starTwoline 56 - lemma
OAI.TamingCompatibility.MetricHodge.formEquiv_starTwoline 59 - def
OAI.TamingCompatibility.MetricHodge.starThreeline 68 - lemma
OAI.TamingCompatibility.MetricHodge.starThree_applyline 72 - lemma
OAI.TamingCompatibility.MetricHodge.starTwo_squareline 97 - lemma
OAI.TamingCompatibility.MetricHodge.starThree_injectiveline 104 - lemma
OAI.TamingCompatibility.MetricHodge.starThree_zeroline 113 - lemma
OAI.TamingCompatibility.MetricHodge.starThree_eq_zeroline 116