OAI/Geometry/TamingCompatibility/DifferentialForms/MetricL2Core.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.MetricForms.pairing_zero_left line 11
2. lemma OAI.TamingCompatibility.MetricForms.pairing_add_left' line 15
3. def OAI.TamingCompatibility.GeometricHilbert.l2Pairing line 31
4. lemma OAI.TamingCompatibility.GeometricHilbert.l2_nonneg line 35
5. lemma OAI.TamingCompatibility.GeometricHilbert.l2_symm line 39
6. def OAI.TamingCompatibility.GeometricHilbert.l2Core line 44
7. def OAI.TamingCompatibility.GeometricHilbert.oneCore line 88
8. def OAI.TamingCompatibility.GeometricHilbert.twoCore line 91