floorRoot_pow_self

Mathlib.Data.Nat.Factorization.Root

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

← MathLib Explorer

English

If n ≠ 0, then floorRoot(n, a^n) = a for all a.

Русский

Если n ≠ 0, тогда floorRoot(n, a^n) = a для любого a.

LaTeX

$$$\forall n\in\mathbb{N},\ n\neq 0\Rightarrow \forall a\in\mathbb{N},\ \text{floorRoot}(n, a^n)=a$$$

Lean4

@[simp]
theorem floorRoot_pow_self (hn : n ≠ 0) (a : ℕ) : floorRoot n (a ^ n) = a := by
  simp [floorRoot_def, pos_iff_ne_zero.2, hn]; split_ifs <;> simp [*]

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

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

Разделы

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

Аффилиация

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