not_pos_pow_dvd

Mathlib.Data.Nat.Init

URI: https://scilib.ai/kg/mathlib#Nat.not_pos_pow_dvd

Lean4

theorem not_pos_pow_dvd {a n : ℕ} (ha : 1 < a) (hn : 1 < n) : ¬a ^ n ∣ a :=
  not_dvd_of_pos_of_lt (Nat.lt_trans Nat.zero_lt_one ha)
    (lt_of_eq_of_lt (Nat.pow_one a).symm ((Nat.pow_lt_pow_iff_right ha).2 hn))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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