Theorem Polynomial.expand_char

Modification history

2026-01-04 10:12
Mathlib/Algebra/Polynomial/Expand.lean
feat(RingTheory/MvPowerSeries): (mv) PowerSeries version of `expand_char` (#33091) …
Deleted Polynomial.expand_charView on Github →
2023-05-19 00:59
Mathlib/Data/Polynomial/Expand.lean
feat: port Data.Polynomial.Expand (#4083)
Added Polynomial.expand_charView on Github →