OAI/GroupTheory/PolycyclicRecognition/Geometry/LieProductDifferential.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The differential of group multiplication at the identity

  1. theorem OAI.PolycyclicRecognition.mfderiv_mul_one line 20
  2. theorem OAI.PolycyclicRecognition.HasMFDerivAt.mul_at_one line 44