OAI/RepresentationTheory/VertexAlgebra/ModuleSharpPolynomial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.PolynomialCutoffControl line 12
2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.polynomialCutoffControl_add line 15
3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.polynomialCutoffControl_sum line 30
4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.polynomialCutoffControl_one line 41
5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.polynomialCutoffControl_root line 44
6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.positiveColumnNorm_sq_polynomial line 53
7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.sharpQuantities_polynomial line 87
8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.sharpMajorant_polynomial line 106