OAI/RepresentationTheory/VertexAlgebra/BicommutantFinite.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StronglyRationalVOA.BicommutantDensity.diagonalHom line 14
  2. theorem OAI.StronglyRationalVOA.BicommutantDensity.diagonalHom_apply line 28
  3. def OAI.StronglyRationalVOA.BicommutantDensity.inclusion line 31
  4. theorem OAI.StronglyRationalVOA.BicommutantDensity.inclusion_apply line 37
  5. theorem OAI.StronglyRationalVOA.BicommutantDensity.sum_inclusion line 43
  6. theorem OAI.StronglyRationalVOA.BicommutantDensity.diagonalHom_inclusion line 48
  7. def OAI.StronglyRationalVOA.BicommutantDensity.entry line 54
  8. theorem OAI.StronglyRationalVOA.BicommutantDensity.entry_apply line 58
  9. theorem OAI.StronglyRationalVOA.BicommutantDensity.apply_eq_sum_entry line 62
  10. theorem OAI.StronglyRationalVOA.BicommutantDensity.entry_commutes line 67
  11. theorem OAI.StronglyRationalVOA.BicommutantDensity.diagonal_commutes_of_entries line 75
  12. theorem OAI.StronglyRationalVOA.BicommutantDensity.diagonal_bicommutant line 87
  13. theorem OAI.StronglyRationalVOA.BicommutantDensity.exists_approx_finite line 112