zmodRepr_eq_zero_iff_dvd

Mathlib.NumberTheory.Padics.RingHoms

URI: https://scilib.ai/kg/mathlib#PadicInt.zmodRepr_eq_zero_iff_dvd

← MathLib Explorer

English

zmodRepr x = 0 iff (p : ℤ_p) divides x.

Русский

zmodRepr(x) = 0 тогда и только тогда, когда p делит x.

LaTeX

$$x.zmodRepr = 0 ↔ (p : ℤ_[p]) ∣ x$$

Lean4

theorem zmodRepr_eq_zero_iff_dvd {x : ℤ_[p]} : x.zmodRepr = 0 ↔ (p : ℤ_[p]) ∣ x :=
  by
  refine ⟨fun H ↦ ?_, zmodRepr_eq_zero_of_dvd⟩
  rw [← norm_lt_one_iff_dvd, ← sub_zero x, ← Nat.cast_zero, ← H]
  exact norm_sub_zmodRepr_lt_one _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru