OAI/Geometry/TamingCompatibility/DifferentialForms/SmoothUnitEvaluation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.eval_antiInvariantPart_complexLine line 27
2. def OAI.TamingCompatibility.smoothUnitEvaluation line 37
3. def OAI.TamingCompatibility.unitMeasureCurrent line 44
4. lemma OAI.TamingCompatibility.unitMeasureCurrent_antiInvariantPart line 59
5. lemma OAI.TamingCompatibility.unitMeasureCurrent_pos line 70
6. lemma OAI.TamingCompatibility.hermitianMetric_unitEvaluation line 89