OAI/Geometry/TamingCompatibility/Hodge/HodgeProjectionRaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HodgeChart.realVectorSchwartz_antiInvariant line 20
2. lemma OAI.TamingCompatibility.HodgeChart.scalarVectorLinear_antiInvariant line 36
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRawDistribution_smooth_antiInvariant line 55
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_laplacian_local_distribution line 100
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_laplacian_power_local_distribution line 115
6. lemma OAI.TamingCompatibility.ComplexMatrix.LocallyEqual.cutoff_self line 143
7. lemma OAI.TamingCompatibility.ComplexMatrix.LocallyEqual.mono line 155
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_commutator_local_distribution line 184