exists_smodEq_untiltAux — Mathlib

English

For every x ∈ PreTilt(O, p), there exists y ∈ O such that for all n, x.untiltAux n ≡ y modulo (p)^n.

Русский

Для каждого x ∈ PreTilt(O, p) существует y ∈ O такой, что для всех n выполняется x.untiltAux n ≡ y mod (p)^n.

LaTeX

$$$\exists y\, \forall n, \ x.untiltAux n \equiv y \pmod{(p)^{n}}$$$

Lean4

theorem exists_smodEq_untiltAux (x : PreTilt O p) :
    ∃ y, ∀ (n : ℕ), x.untiltAux n ≡ y [SMOD Ideal.span {(p : O)} ^ n • (⊤ : Ideal O)] :=
  by
  refine IsPrecomplete.prec' x.untiltAux (fun {m n} h ↦ ?_)
  simpa only [span_singleton_pow, smul_eq_mul, mul_top, SModEq.sub_mem, mem_span_singleton] using
    x.pow_dvd_untiltAux_sub_untiltAux h

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