OAI/Geometry/TamingCompatibility/Hodge/HodgeClosedSmooth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.preStar_self_adjoint line 16
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePreD_adjoint line 21
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeDelta_star_eq_zero_iff line 30
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePreD_closed line 40
5. def OAI.TamingCompatibility.GeometricHilbert.hodgeCoexactPart line 43
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCoexactPart_pair line 47
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCoexactPart_closed_pair line 53
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_closed line 57
9. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_closed_iff line 61