map_val_apply — Mathlib

English

Equality of maps from adic completion to a target can be checked on mk I M a for all a in AdicCauchySequence.

Русский

Сравнение отображений из адического завершения в цель проверяется на образах mk I M a для всех a ∈ AdicCauchySequence.

LaTeX

$$$\forall f,g:\mathrm{AdicCompletion}\ I\ M \to N,\ (\forall a:\mathrm{AdicCauchySequence}\ I\ M,\ f(\mathrm{mk}\ I\ M\ a) = g(\mathrm{mk}\ I\ M\ a)) \Rightarrow f=g$$$

Lean4

@[simp]
theorem map_val_apply (f : M →ₗ[R] N) {n : ℕ} (x : AdicCompletion I M) :
    (map I f x).val n = f.reduceModIdeal (I ^ n) (x.val n) :=
  rfl

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