Commit 2025-12-18 21:53 493ca158

View on Github →

chore(RingTheory/PowerSeries/Expand): tidy up some proofs (#33057) remove erw, classical, reduce to proofs about MvPowerSeries

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Expand.lean

added theorem MvPolynomial.coeff_expand_zero

deleted theorem MvPolynomial.expand_char

modified theorem MvPolynomial.isLocalHom_expand

deleted theorem MvPolynomial.map_expand_pow_char

deleted theorem MvPolynomial.of_irreducible_expand_pow

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Created Mathlib/RingTheory/MvPolynomial/Expand.lean

added theorem MvPolynomial.expand_char

added theorem MvPolynomial.map_expand_char_pow

Modified Mathlib/RingTheory/PowerSeries/Expand.lean