OAI/Analysis/MutuallyUnbiased/MixedMoments/MixedLabelEmbedding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.mixedMoment_label_embedding line 11

   Source documentation

   Injective renaming, including adding unused labels, preserves the moment.

   theorem mixedMoment_label_embedding {p n l k : ℕ} (hk : k ≤ 6) (B : Fin 7 → Basis)
       (A : Matrix (Fin p) (Fin n) ℤ) (e : Fin l ↪ Fin k) (label : Fin n → Fin l) :
       mixedMoment B A (e ∘ label) = mixedMoment B A label := by
   …

   Mentions: OAI.MUB6.Basis, OAI.MUB6.mixedMoment