Theorem MvPolynomial.map_expand_pow_char

Modification history

2025-12-18 21:53
Mathlib/Algebra/MvPolynomial/Expand.lean
chore(RingTheory/PowerSeries/Expand): tidy up some proofs (#33057) …
Deleted MvPolynomial.map_expand_pow_charView on Github →
2025-12-18 09:08
Mathlib/Algebra/MvPolynomial/Expand.lean
feat(RingTheory/MvPowerSeries): some APIs about `expand` (#33005) …
Added MvPolynomial.map_expand_pow_charView on Github →