val_smul_eq_evalₐ_smul — Mathlib

English

For n, r ∈ AdicCompletion I R, and x in the quotient M, r.val n • x equals evalₐ I n r • x.

Русский

Для n, r ∈ AdicCompletion I R и x в модуле M, выполнено r.val n • x = evalₐ I n r • x.

LaTeX

$$val_smul_eq_evalₐ_smul(n, r, x) : r.val n • x = evalₐ(I,n) r • x$$

Lean4

theorem val_smul_eq_evalₐ_smul (n : ℕ) (r : AdicCompletion I R) (x : M ⧸ (I ^ n • ⊤ : Submodule R M)) :
    r.val n • x = evalₐ I n r • x := by
  apply induction_on I R r (fun r ↦ ?_)
  exact Quotient.inductionOn' x (fun x ↦ rfl)

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