not_isUnit_of_mem_primeFactors — Mathlib

English

If p is a prime factor of n, then p modulo n is not a unit in ZMod n.

Русский

Если p является простым делителем n, то p по модулю n не является единицей в ZMod n.

LaTeX

$$$$ p \\in n.primeFactors \\quad\\Rightarrow\\quad ¬\\text{IsUnit}(p : ZMod\\; n) $$$$

Lean4

theorem not_isUnit_of_mem_primeFactors {n p : ℕ} (h : p ∈ n.primeFactors) : ¬IsUnit (p : ZMod n) :=
  by
  rw [isUnit_iff_coprime]
  exact (Prime.dvd_iff_not_coprime <| prime_of_mem_primeFactors h).mp <| dvd_of_mem_primeFactors h

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