OAI/Analysis/Commutator/DerivationCyclicColumns.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.DerivationColumns.Cyclic line 26
  2. theorem OAI.Kadison.DerivationColumns.invariant line 28
  3. lemma OAI.Kadison.DerivationColumns.cyclic_dense line 31
  4. def OAI.Kadison.DerivationColumns.restrictDerivation line 56
  5. lemma OAI.Kadison.DerivationColumns.restrictDerivation_apply line 59
  6. lemma OAI.Kadison.DerivationColumns.restrictDerivation_mul line 63
  7. theorem OAI.Kadison.DerivationColumns.exists_column line 73
  8. def OAI.Kadison.DerivationColumns.column line 80
  9. lemma OAI.Kadison.DerivationColumns.column_spec line 82
  10. lemma OAI.Kadison.DerivationColumns.column_commutator line 86
  11. def OAI.Kadison.DerivationColumns.finiteProjection line 100
  12. def OAI.Kadison.DerivationColumns.finiteImplementer line 102
  13. lemma OAI.Kadison.DerivationColumns.finiteProjection_projection line 105
  14. lemma OAI.Kadison.DerivationColumns.finiteProjection_norm_le line 121
  15. lemma OAI.Kadison.DerivationColumns.finite_column_identity line 124
  16. lemma OAI.Kadison.DerivationColumns.finite_scalar_bound line 129