Theorem Lagrange.leadingCoeff_basis

Modification history

2025-12-08 07:00
Mathlib/LinearAlgebra/Lagrange.lean
feat(LinearAlgebra/Lagrange): Formula for leading coefficient of a polynomial (#32359) …
Added Lagrange.leadingCoeff_basisView on Github →