OAI/RepresentationTheory/FoulkesHowe/FlattenedSwap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.flattenedSymmetricForm_swap_same_row line 11

   Source documentation

   Flattened monomial forms are invariant under any transposition whose slots have the same row.

   theorem flattenedSymmetricForm_swap_same_row {a b : ℕ} {V : Type*}
       [AddCommGroup V] [Module ℂ V] (T : SymmetricMultilinearForm a b V)
       (p q : Fin a × Fin b) (hpq : p.1 = q.1) (v : Fin a × Fin b → V) :
       flattenedSymmetricForm T (v ∘ Equiv.swap p q) = flattenedSymmetricForm T v := by
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.flattenedSymmetricForm

2. theorem OAI.Problem346.flattenedSymmetricForm_coeff_swap_same_row line 24

   Source documentation

   Coefficient arrays of flattened forms satisfy exactly the row-swap condition required to collapse a directional derivative to a multiplicity times one term.

   theorem flattenedSymmetricForm_coeff_swap_same_row {a b : ℕ} {V I : Type*}
       [AddCommGroup V] [Module ℂ V] (T : SymmetricMultilinearForm a b V)
       (e : I → V) (p q : Fin a × Fin b) (hpq : p.1 = q.1)
       (k : Fin a × Fin b → I) :
       flattenedSymmetricForm T (e ∘ (k ∘ Equiv.swap p q)) =
         flattenedSymmetricForm T (e ∘ k) := by
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.flattenedSymmetricForm