OAI/Analysis/Mahler/WedgeAssociativity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.domDomCongr_sum line 12
2. lemma OAI.Mahler.covectorVolume_domDomCongr line 17
3. theorem OAI.Mahler.wedge_assoc line 25

   Source documentation

   Associativity of the actual shuffle product, with the ordered slot reassociation made explicit.

   theorem wedge_assoc (basis : Module.Basis J ℝ T)
       (a : T [⋀^ι]→ₗ[ℝ] ℂ) (b : T [⋀^κ]→ₗ[ℝ] ℂ) (c : T [⋀^ν]→ₗ[ℝ] ℂ) :
       (wedge (wedge a b) c).domDomCongr (Equiv.sumAssoc ι κ ν) = wedge a (wedge b c) := by
   …

   Mentions: OAI.Mahler.wedge

4. theorem OAI.Mahler.wedge_swap line 47

   Source documentation

   Swapping blocks means reindexing by the actual block swap; signs arise when both sides are subsequently put into the same Fin order.

   theorem wedge_swap (basis : Module.Basis J ℝ T)
       (a : T [⋀^ι]→ₗ[ℝ] ℂ) (b : T [⋀^κ]→ₗ[ℝ] ℂ) :
       (wedge a b).domDomCongr (Equiv.sumComm ι κ) = wedge b a := by
   …

   Mentions: OAI.Mahler.wedge