Theorem MvPolynomial.expand_char

Modification history

2026-01-04 10:12

Mathlib/RingTheory/MvPolynomial/Expand.lean

feat(RingTheory/MvPowerSeries): (mv) PowerSeries version of `expand_char` (#33091) …

Deleted MvPolynomial.expand_char View on Github →

2025-12-18 21:53

Mathlib/Algebra/MvPolynomial/Expand.lean

chore(RingTheory/PowerSeries/Expand): tidy up some proofs (#33057) …

Modified MvPolynomial.expand_char View on Github →

2025-12-18 09:08

Mathlib/Algebra/MvPolynomial/Expand.lean

feat(RingTheory/MvPowerSeries): some APIs about `expand` (#33005) …

Added MvPolynomial.expand_char View on Github →