Def HVertexOperator.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) …

Added HVertexOperator.of_coeff View on Github →