OAI/Geometry/Arnold/FieldAlgebra.lean
15 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ArnoldCounterexample.Field.casimir_unitline 15 - lemma
OAI.ArnoldCounterexample.Field.pairing_scaleline 19 - lemma
OAI.ArnoldCounterexample.Field.casimir_scaleline 25 - lemma
OAI.ArnoldCounterexample.Field.mixed_scaleline 28 - lemma
OAI.ArnoldCounterexample.Field.self_scaleline 32 - lemma
OAI.ArnoldCounterexample.Field.core_unitline 36 - lemma
OAI.ArnoldCounterexample.Field.core_homogeneousline 41 - lemma
OAI.ArnoldCounterexample.Field.left_bracketline 56 - lemma
OAI.ArnoldCounterexample.Field.right_bracketline 63 - lemma
OAI.ArnoldCounterexample.Field.mixed_bracketline 70 - lemma
OAI.ArnoldCounterexample.Field.left_core_derivativeline 75 - lemma
OAI.ArnoldCounterexample.Field.right_core_derivativeline 82 - lemma
OAI.ArnoldCounterexample.Field.cross_zero_multiplierline 91 - lemma
OAI.ArnoldCounterexample.Field.core_vertical_criticalline 99 - lemma
OAI.ArnoldCounterexample.Field.core_complex_vertical_criticalline 135