eq_zero_of_gcd_ne_one

Mathlib.Data.ZMod.Coprime

URI: https://scilib.ai/kg/mathlib#ZMod.eq_zero_of_gcd_ne_one

← MathLib Explorer

English

If gcd(a, p) ≠ 1 for a prime p, then a maps to 0 in ZMod p.

Русский

Если gcd(a, p) ≠ 1 для простого p, то a отображается в 0 в ZMod p.

LaTeX

$$$(a \bmod p) = 0$$

Lean4

/-- If an integer `a` and a prime `p` satisfy `gcd a p ≠ 1`, then `a : ZMod p` is zero. -/
theorem eq_zero_of_gcd_ne_one {a : ℤ} {p : ℕ} (pp : p.Prime) (h : a.gcd p ≠ 1) : (a : ZMod p) = 0 :=
  (@eq_zero_iff_gcd_ne_one a p ⟨pp⟩).mpr h

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

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

Разделы

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

Аффилиация

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