ceilRoot_pow_self

Mathlib.Data.Nat.Factorization.Root

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

← MathLib Explorer

English

For every n ≠ 0 and every a ∈ ℕ, ceilRoot n (a^n) = a.

Русский

Для всех n ≠ 0 и всех a ∈ ℕ выполняется ceilRoot n (a^n) = a.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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