Theorem HVertexOperator.of_coeff_coeff

Modification history

2026-09-21 19:06
Mathlib/Algebra/Vertex/HVertexOperator.lean
chore: rename declarations whose names do not match their statements (#44051) …
Modified HVertexOperator.of_coeff_coeffView on Github →
2025-09-16 09:16
Mathlib/Algebra/Vertex/HVertexOperator.lean
chore (Algebra/Vertex): linearize coefficient functions (#29133) …
Added HVertexOperator.of_coeff_coeffView on Github →