Def HVertexOperator.of_coeff

Modification history

2025-09-16 09:16
Mathlib/Algebra/Vertex/HVertexOperator.lean
chore (Algebra/Vertex): linearize coefficient functions (#29133) …
Modified HVertexOperator.of_coeffView on Github →
2024-07-16 01:36
Mathlib/Algebra/Vertex/HVertexOperator.lean
fix (Algebra/Vertex/HVertexOperator): rm defeq abuse in coeff function (#13422) …
Added HVertexOperator.of_coeffView on Github →