OAI/Geometry/TamingCompatibility/Hodge/HodgeLocalCoefficients.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.exists_hodge_local_coefficients line 26
2. def OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_power_commutator_lift line 77
3. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_power_commutator_lift_spec line 89
4. lemma OAI.TamingCompatibility.ComplexMatrix.normalizedFullSquare_power_commutator_lift_zero_spec line 100
5. lemma OAI.TamingCompatibility.ComplexMatrix.normalized_commutator_localized_spec line 122
6. lemma OAI.TamingCompatibility.bounded_triple_composition line 145