dvd_ceilRoot_pow

Mathlib.Data.Nat.Factorization.Root

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

English

For n ≠ 0, a ∣ ceilRoot n a^n.

Русский

Для n ≠ 0 выполняется a делится на (ceilRoot n a)^n.

LaTeX

$$$ \forall a,n \in \mathbb{N}, n \neq 0 \Rightarrow a \mid (\operatorname{ceilRoot}(n,a))^n $$$

Lean4

theorem dvd_ceilRoot_pow (hn : n ≠ 0) : a ∣ ceilRoot n a ^ n :=
  (dvd_pow_iff_ceilRoot_dvd hn).2 dvd_rfl

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

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

Разделы

Аффилиация

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