val_add_apply — Mathlib

English

Let I be an ideal in a commutative ring R and M an R-module. For any f,g in the I-adic completion of M and any n in N, the valuation map is additive: (f + g).val(n) = f.val(n) + g.val(n).

Русский

Пусть I — идеал в коммутативном кольце R и M — модуль над R. Для любых f,g ∈ I-адического дополнения M и любого n ∈ ℕ выполняется: (f + g).val(n) = f.val(n) + g.val(n).

LaTeX

$$$ \\forall f,g \\in \\mathrm{AdicCompletion}(I,M), \\forall n \\in \\mathbb{N}, (f+g).val(n) = f.val(n) + g.val(n) $$$

Lean4

theorem val_add_apply (f g : AdicCompletion I M) (n : ℕ) : (f + g).val n = f.val n + g.val n :=
  rfl

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