OAI/RepresentationTheory/VertexAlgebra/BoundedIntertwinerFinite.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.StronglyRationalVOA.BoundedIntertwiner.SumSpace line 12
2. def OAI.StronglyRationalVOA.BoundedIntertwiner.row line 14
3. theorem OAI.StronglyRationalVOA.BoundedIntertwiner.row_apply line 17
4. def OAI.StronglyRationalVOA.BoundedIntertwiner.column line 20
5. theorem OAI.StronglyRationalVOA.BoundedIntertwiner.column_apply line 24
6. theorem OAI.StronglyRationalVOA.BoundedIntertwiner.row_adjoint line 27
7. def OAI.StronglyRationalVOA.BoundedIntertwiner.diagonal line 34
8. theorem OAI.StronglyRationalVOA.BoundedIntertwiner.diagonal_apply line 38
9. theorem OAI.StronglyRationalVOA.BoundedIntertwiner.norm_diagonal_le line 42
10. theorem OAI.StronglyRationalVOA.BoundedIntertwiner.norm_sum_le line 52