hasBasis_nhds_zero — Mathlib

English

If I is an adic ideal, then the neighborhood system at 0 has a basis consisting of the powers I^n.

Русский

Если I — адическая идея, то окрестности нуля имеют базис из степеней I^n.

LaTeX

$$$(\mathcal{N}(0))\\HasBasis (\\lambda _ \to True) (\\lambda n \\to ↑(I^n))$$$

Lean4

theorem hasBasis_nhds_zero {I : Ideal R} (hI : IsAdic I) : (𝓝 (0 : R)).HasBasis (fun _ ↦ True) fun n ↦ ↑(I ^ n) :=
  hI ▸ Ideal.hasBasis_nhds_zero_adic I

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