OAI/Analysis/Mahler/SourceRawOrientation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.rawPrefix_firstJet line 14
2. lemma OAI.Mahler.rawProduct_reindex_left line 21
3. lemma OAI.Mahler.rawMain_firstJet line 30
4. def OAI.Mahler.sourceTopSlots line 43

   Source documentation

   Explicit order of the differentiated top form: first the two slots created from derivative and one-form, then all existing interleaved pairs.

   def sourceTopSlots (k : ℕ) : WedgePowerSlots (k+1) ≃ Fin ((2*k+1)+1) :=
   …

   Mentions: OAI.Mahler.WedgePowerSlots