isUnit_ofNat_iff

Mathlib.Algebra.CharP.Invertible

URI: https://scilib.ai/kg/mathlib#CharP.isUnit_ofNat_iff

English

For n ≥ 2 and prime p, IsUnit (ofNat(n) : R) iff ¬p ∣ ofNat(n).

Русский

Для n ≥ 2 и простого p выполняется IsUnit(ofNat(n) : R) эквивалентно ¬ p ∣ ofNat(n).

LaTeX

$$IsUnit(ofNat(n) : R) \iff ¬ p ∣ ofNat(n)$$

Lean4

theorem isUnit_ofNat_iff {n : ℕ} [n.AtLeastTwo] (hp : p.Prime) : IsUnit (ofNat(n) : R) ↔ ¬p ∣ ofNat(n) :=
  CharP.isUnit_natCast_iff hp

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

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

Разделы

Аффилиация

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