Theorem MvPowerSeries.IsNilpotent_subst

Modification history

2026-06-30 06:44
Mathlib/RingTheory/MvPowerSeries/Substitution.lean
feat(FormalGroup): `F(X,0)=X` and `F(0,X)=X` (#38052) …
Modified MvPowerSeries.IsNilpotent_substView on Github →
2025-04-02 07:08
Mathlib/RingTheory/MvPowerSeries/Substitution.lean
feat(MvPowerSeries/Substitution): substitution of power series inside power series (#15158) …
Added MvPowerSeries.IsNilpotent_substView on Github →