untiltAux_smodEq_untiltFun — Mathlib

English

For all x ∈ PreTilt(O, p) and every n, x.untiltAux n ≡ x.untiltFun modulo (p^n) span, i.e., they are congruent in the Smod sense.

Русский

Для всех x ∈ PreTilt(O, p) и всякого n, x.untiltAux n эквивалентно x.untiltFun по модулю (p^n).

LaTeX

$$$\forall n, x.untiltAux n \equiv x.untiltFun \; [SMOD (span\{(p:O)\})^n]$$$

Lean4

theorem untiltAux_smodEq_untiltFun (x : PreTilt O p) (n : ℕ) :
    x.untiltAux n ≡ x.untiltFun [SMOD (span {(p : O)}) ^ n] := by
  simpa [untiltFun] using Classical.choose_spec x.exists_smodEq_untiltAux n

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