English
If the base ring is linear-topological and the constant coefficient of a mv-power-series f is topologically nilpotent, then f itself is topologically nilpotent.
Русский
Пусть база имеет линейную топологию; если константный коэффициент mv-рядf является топологически нильпотентным, то сам ряд f является топологически нильпотентным.
LaTeX
$$$\text{If } f\in \mathrm{MvPowerSeries}(\sigma,R)\text{ and } \mathrm{constantCoeff}(f)\in \mathrm{IsTopologicallyNilpotent}(R) ,\ \text{then } f\text{ is topologically nilpotent}.$$$
Lean4
theorem isTopologicallyNilpotent_of_constantCoeff {R : Type*} [CommRing R] [TopologicalSpace R] [IsLinearTopology R R]
{f : MvPowerSeries σ R} (hf : IsTopologicallyNilpotent (constantCoeff f)) : IsTopologicallyNilpotent f :=
by
simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero,
IsLinearTopology.hasBasis_ideal.tendsto_right_iff]
intro d I hI
replace hf := hf.eventually_mem hI
simp_rw [eventually_atTop, SetLike.mem_coe, ← Ideal.Quotient.eq_zero_iff_mem, map_pow, ← coeff_map, ←
constantCoeff_map] at hf ⊢
obtain ⟨N, hN⟩ := hf
use N + d.degree
intro n hn
simpa only [map_pow] using coeff_eq_zero_of_constantCoeff_nilpotent (hN N le_rfl) hn
