OAI/InformationTheory/QuantumCircuit/Count.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QAC.tensorMatrix_smul line 11
  2. lemma OAI.QAC.tensorMatrix_nonneg line 18
  3. lemma OAI.QAC.tensorMatrix_le_one line 30
  4. def OAI.QAC.Count.empty line 43
  5. lemma OAI.QAC.Count.empty_zero line 48
  6. def OAI.QAC.Count.join line 51
  7. lemma OAI.QAC.Count.join_zero line 60
  8. lemma OAI.QAC.Count.disjoint_commute line 72
  9. def OAI.QAC.Count.restrict line 86

    Source documentation

    Subcounts with the same axes, allowing repeated monomial indices to collapse.

    def Count.restrict {N : ℕ} (M : Count N) (S : Finset (Fin N)) : Count N where
…

    Mentions: OAI.QAC.Count

  10. lemma OAI.QAC.Count.restrict_zero_mul line 91
  11. lemma OAI.QAC.Count.restrict_support_card line 103