eval_of — Mathlib

English

For x in M, evaluating the image of x under AdicCompletion at n yields the coset mkQ of x modulo I^n • ⊤, i.e., eval I M n (of I M x) = mkQ (I^n • ⊤) x.

Русский

Для x ∈ M вычисление в координате n образа x под AdicCompletion даёт класс по модулю I^n • ⊤: eval I M n (of I M x) = mkQ (I^n • ⊤) x.

LaTeX

$$$ eval\\, I\\, M\\, n\\ (of\\, I\\, M\\ x) = mkQ(I^n \\cdot \\top : Submodule\\, R\\, M)\\ x $$$

Lean4

theorem eval_of (n : ℕ) (x : M) : eval I M n (of I M x) = mkQ (I ^ n • ⊤ : Submodule R M) x :=
  rfl

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