OAI/Geometry/TamingCompatibility/Hodge/HodgeMixing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_regularized_positive_current_mixing line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_relative_complement line 52
3. lemma OAI.TamingCompatibility.GeometricHilbert.antiProjection_pair_split line 79
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_regularized_positive_current_cross line 103