isUnit_prime_of_not_dvd — Mathlib

English

Let p be a prime and n a natural number. If p does not divide n, then p mod n is a unit in ZMod n.

Русский

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

LaTeX

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

Lean4

theorem isUnit_prime_of_not_dvd {n p : ℕ} (hp : p.Prime) (h : ¬p ∣ n) : IsUnit (p : ZMod n) :=
  (isUnit_prime_iff_not_dvd hp).mpr h

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