OAI/Geometry/TamingCompatibility/DifferentialForms/Hermitian.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ManifoldForms.ddc_zero_off line 18
2. lemma OAI.TamingCompatibility.ManifoldForms.chartLift_tsupport_subset line 27
3. lemma OAI.TamingCompatibility.GeometricChart.rawPair_zero_of_zero line 41
4. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.logSource_zero_off line 64
5. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.sqrtSource_zero_off line 77
6. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.logSource_dual_uniform line 101
7. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.sqrtSource_dual_uniform line 111