OAI/GroupTheory/PolycyclicRecognition/Algebra/RightTranslationInvariant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Right translation of an invariant vector field

The change in a left-invariant field under right multiplication is the actual differential of conjugation. No representation is used.

  1. theorem OAI.PolycyclicRecognition.mfderiv_mul_right_invariant line 20
  2. theorem OAI.PolycyclicRecognition.mfderiv_mul_right_inverse_invariant line 59