floorRoot_pow_dvd

Mathlib.Data.Nat.Factorization.Root

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

English

For all a,n, floorRoot(n,a) raised to the power n divides a.

Русский

Для всех a,n: floorRoot(n,a)^n делит a.

LaTeX

$$$\text{floorRoot}(n,a)^n \mid a$$$

Lean4

theorem floorRoot_pow_dvd : floorRoot n a ^ n ∣ a :=
  pow_dvd_iff_dvd_floorRoot.2 dvd_rfl

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

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

Разделы

Аффилиация

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