OAI/RepresentationTheory/VertexAlgebra/BoundedIntertwinerCore.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StronglyRationalVOA.BoundedIntertwiner.coreline 12 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.core_applyline 14 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.core_singleline 16 - def
OAI.StronglyRationalVOA.BoundedIntertwiner.coreActline 20 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.coreAct_applyline 22 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.coreAct_singleline 24 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.norm_coreAct_leline 30 - def
OAI.StronglyRationalVOA.BoundedIntertwiner.actionline 42 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.action_coreline 45 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.action_intertwinesline 50 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.norm_action_leline 55 - theorem
OAI.StronglyRationalVOA.BoundedIntertwiner.ext_of_totalline 61