Commit 2026-01-04 10:12 e26801b2

View on Github →

feat(RingTheory/MvPowerSeries): (mv) PowerSeries version of expand_char (#33091) I proved the expand_char for (mv) power series. And also unify the expand for (mv) polynomial and (mv) power series.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Expand.lean

deleted theorem Polynomial.expand_char

deleted theorem Polynomial.map_expand_pow_char

added theorem Polynomial.map_frobenius_expand

added theorem Polynomial.map_iterateFrobenius_expand

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/Perfect.lean

Modified Mathlib/RingTheory/MvPolynomial/Expand.lean

deleted theorem MvPolynomial.expand_char

deleted theorem MvPolynomial.map_expand_char_pow

added theorem MvPolynomial.map_frobenius_expand

added theorem MvPolynomial.map_iterateFrobenius_expand

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

added theorem MvPowerSeries.map_map

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

added theorem MvPowerSeries.expand_eq_expand

added theorem MvPowerSeries.map_frobenius_expand

added theorem MvPowerSeries.map_iterateFrobenius_expand

added theorem MvPowerSeries.trunc'_expand

added theorem MvPowerSeries.trunc'_expand_trunc'

Modified Mathlib/RingTheory/MvPowerSeries/Trunc.lean

added theorem MvPowerSeries.eq_iff_frequently_trunc'_eq

added theorem MvPowerSeries.ext_trunc'

added theorem MvPowerSeries.totalDegree_trunc'

added theorem MvPowerSeries.trunc'_trunc'

added theorem MvPowerSeries.trunc'_trunc'_pow

Modified Mathlib/RingTheory/PowerSeries/Expand.lean