of_apply — Mathlib

English

Let x be in M. The image of x under the natural map of AdicCompletion is given coordinate-wise by mkQ: (of I M x).1 n = mkQ (I^n • ⊤) x.

Русский

Пусть x ∈ M. Образ x под естественным отображением AdicCompletion задан координатно: (of I M x).1 n = mkQ (I^n • ⊤) x.

LaTeX

$$$ (\\mathrm{of}\\, I\\, M\\ x).1(n) = \\mathrm{mkQ}(I^n \\cdot \\top : \\mathrm{Submodule}\, R\, M)\\ x $$$

Lean4

@[simp]
theorem of_apply (x : M) (n : ℕ) : (of I M x).1 n = mkQ (I ^ n • ⊤ : Submodule R M) x :=
  rfl

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