OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianTraceTranslation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ExteriorForms.extDeriv_dc_translate line 14
2. lemma OAI.TamingCompatibility.ExteriorForms.extDeriv_dc_congr_germ line 25
3. lemma OAI.TamingCompatibility.RadialPotential.schwartz_hermitianLog_lower line 39
4. lemma OAI.TamingCompatibility.RadialPotential.schwartz_hermitianSqrt_lower line 59