not_isPrimePow

Mathlib.Algebra.IsPrimePow

URI: https://scilib.ai/kg/mathlib#IsUnit.not_isPrimePow

English

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

Русский

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

LaTeX

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

Lean4

theorem not_isPrimePow {n : R} (h : IsUnit n) : ¬IsPrimePow n := fun h' => h'.not_unit h

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

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

Разделы

Аффилиация

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