OAI/Geometry/TamingCompatibility/Hodge/HodgeCommutatorPowers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare line 17
2. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_order line 22
3. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_commutator_order line 31
4. lemma OAI.TamingCompatibility.ComplexMatrix.operator_power_order line 43
5. lemma OAI.TamingCompatibility.ComplexMatrix.operator_power_commutator_order line 57
6. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_power_commutator_order line 85
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_laplacian_weighted_distribution line 115