Theorem MvPolynomial.expand_one_apply

Modification history

2025-10-27 15:02
Mathlib/Algebra/MvPolynomial/Expand.lean
feat(MvPolynomial/Expand): more lemmas (#28833)
Modified MvPolynomial.expand_one_applyView on Github →
2023-04-04 12:51
Mathlib/Data/MvPolynomial/Expand.lean
feat: port Data.MvPolynomial.Expand (#3261)
Added MvPolynomial.expand_one_applyView on Github →