OAI/GroupTheory/PolycyclicRecognition/Geometry/FlowDerivativeIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiating compactly supported pairings along horizontal flows

  1. theorem OAI.PolycyclicRecognition.eventually_compact_right_flow_mem line 16
  2. theorem OAI.PolycyclicRecognition.hasDerivAt_integral_right_flow line 33