ext_of_toZModPow — Mathlib

English

Equivalence of PadicInt is determined by all projections to ZModPow: two elements x,y ∈ ℤ_[p] are equal iff for all n, toZModPow n x = toZModPow n y.

Русский

Эквивалентность элементов ℤ_[p] определяется по всем проекциям в ZModPow: x = y тогда и только тогда, когда для всех n выполняется toZModPow n x = toZModPow n y.

LaTeX

$$$\\big( \\forall n, toZModPow\\, n\\ x = toZModPow\\, n\\ y \\big) \\iff x = y$$$

Lean4

theorem ext_of_toZModPow {x y : ℤ_[p]} : (∀ n, toZModPow n x = toZModPow n y) ↔ x = y :=
  by
  constructor
  · intro h
    rw [← lift_self x, ← lift_self y]
    simp +unfoldPartialApp [lift, limNthHom, nthHom, h]
  · rintro rfl _
    rfl

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