cpow_nat_inv_pow

Mathlib.Analysis.SpecialFunctions.Pow.Complex

URI: https://scilib.ai/kg/mathlib#Complex.cpow_nat_inv_pow

← MathLib Explorer

English

For any x ∈ ℂ and natural n with n ≠ 0, (x^(1/n))^n = x.

Русский

Для любого x ∈ ℂ и натурального n, не равного нулю, (x^(1/n))^n = x.

LaTeX

$$$\left(x^{(n^{-1})}\right)^{n} = x$$$

Lean4

@[simp]
theorem cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) : (x ^ (n⁻¹ : ℂ)) ^ n = x :=
  by
  rw [← cpow_nat_mul, mul_inv_cancel₀, cpow_one]
  assumption_mod_cast

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

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

Разделы

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

Аффилиация

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