OAI/Geometry/SplitTangent/LeadingJetProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Leading Jet Product.

  1. lemma OAI.SplitTangent.LeadingJet.iteratedFDeriv_smul_zero line 14
  2. theorem OAI.SplitTangent.LeadingJet.iteratedFDeriv_smul_of_lower_zero line 43