isTopologicallyNilpotent_of_constantCoeff_isNilpotent

English

If the constant coefficient of f is nilpotent, then f is topologically nilpotent.

Русский

Если константный коэффициент f является nilpotent, то f является топологически нильпотентным.

LaTeX

$$IsNilpotent(constantCoeff f) → IsTopologicallyNilpotent f$$

Lean4

theorem isTopologicallyNilpotent_of_constantCoeff_isNilpotent [CommSemiring R] {f : MvPowerSeries σ R}
    (hf : IsNilpotent (constantCoeff f)) : IsTopologicallyNilpotent f := by
  classical
  obtain ⟨m, hm⟩ := hf
  simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero]
  exact fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦ coeff_eq_zero_of_constantCoeff_nilpotent hm hn

Похожие утверждения