OAI/Analysis/MutuallyUnbiased/Bases/Families.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Restriction and cardinality lemmas. These reductions do not establish the no-seven or completion theorem, which remain separate proof obligations.

  1. theorem OAI.MUB6.IsMUBFamily.reindex line 11
  2. theorem OAI.MUB6.attainable_mono line 16
  3. theorem OAI.MUB6.attainable_zero line 21
  4. def OAI.MUB6.SixExtendToSeven line 27

    Source documentation

    Precise completion statement, including preservation of the original bases.

    def SixExtendToSeven : Prop :=
…
  5. theorem OAI.MUB6.no_six_of_completion line 31
  6. theorem OAI.MUB6.family_size_le_five_of_no_six line 37
  7. theorem OAI.MUB6.N6_le_five_of_no_six line 43