Commit 2024-12-05 10:46 67d092e3

View on Github →

feat(Algebra/Vertex): Define vertex operators (#19298) A vertex operator for an R-module V is an R-module map from V to Laurent series on V. This PR defines vertex operators and introduces a normalized indexing for coefficients.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

added theorem HVertexOperator.add_coeff

added theorem HVertexOperator.smul_coeff

Created Mathlib/Algebra/Vertex/VertexOperator.lean

added theorem VertexOperator.coeff_eq_ncoeff

added theorem VertexOperator.coeff_eq_zero_of_lt_order

added theorem VertexOperator.ext

added def VertexOperator.ncoeff

added theorem VertexOperator.ncoeff_add

added theorem VertexOperator.ncoeff_eq_zero_of_lt_order

added theorem VertexOperator.ncoeff_of_coeff

added theorem VertexOperator.ncoeff_smul

added theorem VertexOperator.of_coeff_apply_coeff

Modified docs/references.bib