English
A detailed technical formulation showing mk I M f = 0 under the previously stated tail condition.
Русский
Подробная техническая формулировка, показывающая, что mk I M f = 0 при заданном условиях хвоста.
LaTeX
$$$ \\text{mk I M } f = 0 \\; \\text{under tail condition described above}$$$
Lean4
/-- Criterion for checking that an adic Cauchy sequence is mapped to zero in the adic completion. -/
theorem mk_zero_of (f : AdicCauchySequence I M)
(h : ∃ k : ℕ, ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, f m ∈ (I ^ l • ⊤ : Submodule R M)) : AdicCompletion.mk I M f = 0 :=
by
obtain ⟨k, h⟩ := h
ext n
obtain ⟨m, hnm, l, hnl, hl⟩ := h (n + k) (by cutsat)
rw [mk_apply_coe, Submodule.mkQ_apply, val_zero, ← AdicCauchySequence.mk_eq_mk (show n ≤ m by cutsat)]
simpa using (Submodule.smul_mono_left (Ideal.pow_le_pow_right (by cutsat))) hl
