Theorem MvPowerSeries.subst_sub

Modification history

2026-03-21 06:41
Mathlib/RingTheory/MvPowerSeries/Substitution.lean
feat(MvPowerSeries): subst_C and omit some finiteness of index set (#35842)
Added MvPowerSeries.subst_subView on Github →