Theorem MvPowerSeries.trunc'_expand_trunc'

Modification history

2026-01-04 10:12

Mathlib/RingTheory/MvPowerSeries/Expand.lean

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

Added MvPowerSeries.trunc'_expand_trunc'View on Github →