not_unit

Mathlib.Algebra.IsPrimePow

URI: https://scilib.ai/kg/mathlib#IsPrimePow.not_unit

English

If n is a prime power then it is not a unit.

Русский

Если число является степенью простого, то оно не является единицей.

LaTeX

$$$\text{IsPrimePow } n \;\rightarrow\; \lnot \text{IsUnit } n$$$

Lean4

theorem not_unit {n : R} (h : IsPrimePow n) : ¬IsUnit n :=
  let ⟨_p, _k, hp, hk, hn⟩ := h
  hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_unit

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

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

Разделы

Аффилиация

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