OAI/GroupTheory/PolycyclicRecognition/Algebra/SuspendedVectorFieldBracket.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Differentiating a transported field along time

The bracket of the constant time field with a vertical field is its time derivative. Naturality of brackets then identifies the derivative of a field transported by a flow, without a separate mixed-partial computation.

  1. theorem OAI.PolycyclicRecognition.fderiv_prod_apply_fst line 23
  2. theorem OAI.PolycyclicRecognition.fderiv_prod_apply_snd line 33
  3. theorem OAI.PolycyclicRecognition.lieBracket_time_vertical line 43
  4. theorem OAI.PolycyclicRecognition.lieBracket_suspended_vertical line 53
  5. theorem OAI.PolycyclicRecognition.transportedField_time_derivative line 68