OAI/RepresentationTheory/FoulkesHowe/FoulkesSymmetries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.symMonomial_perm_reindex line 13

   Source documentation

   Reindexing the factors of a symmetric monomial does not change it.

   theorem symMonomial_perm_reindex (n : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V] (v : Fin n → V)
       (τ : Equiv.Perm (Fin n)) :
       symMonomial n V (fun i => v (τ i)) = symMonomial n V v := by
   …

   Mentions: OAI.Problem346.symMonomial

2. theorem OAI.Problem346.foulkesFormula_inner_permute line 22

   Source documentation

   The canonical averaging formula is invariant under independent permutations of the entries in each row.

   theorem foulkesFormula_inner_permute (a b : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V] (v : Fin b → Fin a → V)
       (τ : Fin b → Equiv.Perm (Fin a)) :
       foulkesFormula a b V (fun j i => v j (τ j i)) =
         foulkesFormula a b V v := by
   …

   Mentions: OAI.Problem346.foulkesFormula

3. theorem OAI.Problem346.foulkesFormula_outer_permute line 34

   Source documentation

   The canonical averaging formula is invariant under permutation of rows.

   theorem foulkesFormula_outer_permute (a b : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V] (v : Fin b → Fin a → V)
       (τ : Equiv.Perm (Fin b)) :
       foulkesFormula a b V (fun j i => v (τ j) i) =
         foulkesFormula a b V v := by
   …

   Mentions: OAI.Problem346.foulkesFormula