OAI/Analysis/Mahler/PairExteriorBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.pairExterior_is_wedge line 13

   Source documentation

   The continuous primitive is the shuffle wedge, with its two slots kept in their specified order.

   lemma pairExterior_is_wedge (a b : E →L[ℝ] ℂ) :
       (pairExterior a b).toAlternatingMap =
         (wedge (oneForm (fun _ : E => a) 0).toAlternatingMap
           (oneForm (fun _ : E => b) 0).toAlternatingMap).domDomCongr (prependFinEquiv 1) := by
   …

   Mentions: OAI.Mahler.pairExterior, OAI.Mahler.wedge, OAI.Mahler.oneForm, OAI.Mahler.prependFinEquiv