Theorem Lagrange.nodal_eq_mul_nodal_erase

Modification history

2023-09-07 00:04

Mathlib/LinearAlgebra/Lagrange.lean

feat(LinearAlgebra/Lagrange): Generalize typeclasses. (#6714) …

Modified Lagrange.nodal_eq_mul_nodal_erase View on Github →

2023-05-06 07:17

Mathlib/LinearAlgebra/Lagrange.lean

feat: port LinearAlgebra.Lagrange (#3784)

Added Lagrange.nodal_eq_mul_nodal_erase View on Github →