Def VertexAlg.HetVertexOperator.of_coeff

Modification history

2024-07-16 01:36

Mathlib/Algebra/Vertex/HVertexOperator.lean

fix (Algebra/Vertex/HVertexOperator): rm defeq abuse in coeff function (#13422) …

Deleted VertexAlg.HetVertexOperator.of_coeff View on Github →

2024-05-17 07:11

Mathlib/Algebra/Vertex/HVertexOperator.lean

feat (Algebra/Vertex) Heterogeneous vertex operators (#11797) …

Added VertexAlg.HetVertexOperator.of_coeff View on Github →