Theorem MvPolynomial.map_expand_char_pow

Modification history

2026-01-04 10:12
Mathlib/RingTheory/MvPolynomial/Expand.lean
feat(RingTheory/MvPowerSeries): (mv) PowerSeries version of `expand_char` (#33091) …
Deleted MvPolynomial.map_expand_char_powView on Github →
2025-12-18 21:53
Mathlib/RingTheory/MvPolynomial/Expand.lean
chore(RingTheory/PowerSeries/Expand): tidy up some proofs (#33057) …
Added MvPolynomial.map_expand_char_powView on Github →