OAI/Geometry/TamingCompatibility/Hodge/HodgeScalarSquare.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ComplexMatrix.fullPrincipalScalar line 19
2. lemma OAI.TamingCompatibility.ComplexMatrix.fullPrincipalScalar_apply line 23
3. lemma OAI.TamingCompatibility.ComplexMatrix.fullPrincipalMatrix_scalar line 34
4. def OAI.TamingCompatibility.ComplexMatrix.fullWeightedAdj line 52
5. lemma OAI.TamingCompatibility.ComplexMatrix.full_square_scalar_expansion line 56
6. def OAI.TamingCompatibility.HodgeChart.patchA line 90
7. def OAI.TamingCompatibility.HodgeChart.patchB line 93
8. lemma OAI.TamingCompatibility.HodgeChart.patch_normal line 96
9. lemma OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol_weighted_polarized line 115
10. lemma OAI.TamingCompatibility.HodgeChart.patchA_polarized line 141
11. lemma OAI.TamingCompatibility.HodgeChart.patch_principal_apply line 147