Commit 2026-08-27 11:15 41546748

View on Github →

feat(FieldTheory/Finite): add variant theorems for expand_card (#39219) Add MvPolynomial, MvPowerSeries, PowerSeries version of FiniteField.expand_card, which is only for polynomial.

Estimated changes

Modified Mathlib/FieldTheory/Finite/Basic.lean

added theorem FiniteField.Polynomial.expand_card

deleted theorem FiniteField.expand_card

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

Modified Mathlib/RingTheory/MvPolynomial/Expand.lean

added theorem FiniteField.MvPolynomial.expand_card

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

added theorem FiniteField.MvPowerSeries.expand_card

Modified Mathlib/RingTheory/PowerSeries/Expand.lean

added theorem FiniteField.PowerSeries.expand_card

added theorem PowerSeries.map_frobenius_expand

added theorem PowerSeries.map_iterateFrobenius_expand