Theorem HVertexOperator.compHahnSeries_add

Modification history

2024-07-17 20:56
Mathlib/Algebra/Vertex/HVertexOperator.lean
feat (Algebra/Vertex/HVertexOperator) : Composite heterogeneous vertex operators (#12998) …
Added HVertexOperator.compHahnSeries_addView on Github →