Commit 2025-09-16 09:16 76a3eef4

View on Github →

chore (Algebra/Vertex): linearize coefficient functions (#29133) This PR upgrades the coefficient functions of vertex operators and heterogeneous vertex operators to be linear maps instead of just functions. We also deprecate the corresponding linearity lemmas, and add two rfl simp lemmas.

Estimated changes

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

modified def HVertexOperator.coeff

deleted theorem HVertexOperator.coeff_add

modified theorem HVertexOperator.coeff_inj

added theorem HVertexOperator.coeff_of_coeff

deleted theorem HVertexOperator.coeff_smul

modified def HVertexOperator.of_coeff

added theorem HVertexOperator.of_coeff_coeff

Modified Mathlib/Algebra/Vertex/VertexOperator.lean

modified def VertexOperator.ncoeff

deleted theorem VertexOperator.ncoeff_add

added theorem VertexOperator.ncoeff_apply

deleted theorem VertexOperator.ncoeff_smul