OAI/Geometry/Immersion/ClosedSurface/DoubleModes.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ClosedSurfaceR4.RealModes.realOsc_negline 13 - lemma
OAI.ClosedSurfaceR4.RealModes.realLinearized_add_rightline 18 - lemma
OAI.ClosedSurfaceR4.RealModes.realMetricTensor_addline 25 - lemma
OAI.ClosedSurfaceR4.RealModes.single_phase_metric_identityline 34 - def
OAI.ClosedSurfaceR4.RealModes.doubleCancelAmplitudeline 62 - def
OAI.ClosedSurfaceR4.RealModes.doubleCancelFieldline 66 - theorem
OAI.ClosedSurfaceR4.RealModes.weighted_doubleCancellerline 69