transitionMap_comp_eval — Mathlib

English

Unraveling the defining property of an AdicCauchySequence, the quotient equalities mk (f.val n) = mk (f.val m) hold when m ≤ n in a suitable sense.

Русский

Развернутое определение AdicCauchySequence: равенства mk (f.val n) = mk (f.val m) при m ≤ n

LaTeX

$$$ \\forall m \\le n, \\; Submodule.Quotient.mk (p := (I^m \\cdot \\top)) (f.n) = Submodule.Quotient.mk (p := (I^m \\cdot \\top)) (f.m) $$$

Lean4

@[simp]
theorem transitionMap_comp_eval {m n : ℕ} (hmn : m ≤ n) : transitionMap I M hmn ∘ₗ eval I M n = eval I M m :=
  by
  ext x
  simp

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