val_smul — Mathlib

English

Let I be an ideal in a commutative ring R, M an R-module, and S a ring acting compatibly. For s in S and f in AdicCompletion I M, the scalar action commutes with val: (s • f).val = s • (f.val).

Русский

Пусть I — идеал, M — модуль над R, и S действует совместно. Тогда для любого s ∈ S и f ∈ AdicCompletion I M выполняется (s • f).val = s • (f.val).

LaTeX

$$$ \\forall s \\in S, \\forall f \\in \\mathrm{AdicCompletion}(I,M), (s \\cdot f).val = s \\cdot f.val $$$

Lean4

@[norm_cast]
theorem val_smul [SMul S R] [SMul S M] [IsScalarTower S R M] (s : S) (f : AdicCompletion I M) :
    (s • f).val = s • f.val :=
  rfl

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