eval_apply — Mathlib

English

Evaluating at n after applying AdicCompletion yields the nth coordinate of the element, i.e., (eval I M n) f = f.val n.

Русский

При вычислении в позиции n после применения AdicCompletion получаем n-ую координату элемента: (eval I M n) f = f.val n.

LaTeX

$$$ (\\mathrm{eval}\\, I\\, M\\, n)\\; f = f.\\mathrm{val}(n) $$$

Lean4

theorem eval_apply (n : ℕ) (f : AdicCompletion I M) : eval I M n f = f.1 n :=
  rfl

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