coe_eval — Mathlib

English

The evaluation map from AdicCompletion to the quotient M / (I^n • ⊤) corresponds to the nth coordinate of f, i.e., (eval I M n) corresponds to the projection onto f.n.

Русский

Отображение eval из AdicCompletion в фактор-пространство M / (I^n • ⊤) совпадает с n-ой координатой элемента f.

LaTeX

$$$ (\\mathrm{eval}\\, I\\, M\\, n) = (\\lambda f, f.1\\ n) $$$

Lean4

@[simp]
theorem coe_eval (n : ℕ) : (eval I M n : AdicCompletion I M → M ⧸ (I ^ n • ⊤ : Submodule R M)) = fun f => f.1 n :=
  rfl

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