isUnit_prime_iff_not_dvd — Mathlib

English

Let p be a prime and n a natural number. Then p mod n is a unit in ZMod n if and only if p does not divide n.

Русский

Пусть p — простое число и n — натуральное число. Тогда p по модулю n является единицей в ZMod n тогда и только если p не делит n.

LaTeX

$$$IsUnit\bigl(p : \mathbb{Z}/n\mathbb{Z}\bigr) \iff \neg (p \mid n)$$$

Lean4

theorem isUnit_prime_iff_not_dvd {n p : ℕ} (hp : p.Prime) : IsUnit (p : ZMod n) ↔ ¬p ∣ n := by
  rw [isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd hp]

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