Theorem LaurentPolynomial.smeval_single

Modification history

2025-12-12 18:47
Mathlib/Algebra/Polynomial/Laurent.lean
chore(Algebra/MonoidAlgebra): reduce dependence on defeq abuse, golf (#32604) …
Modified LaurentPolynomial.smeval_singleView on Github →
2024-12-20 09:05
Mathlib/Algebra/Polynomial/Laurent.lean
feat(Algebra/Polynomial/Laurent): evaluate at a unit (#19617) …
Added LaurentPolynomial.smeval_singleView on Github →