exists_pow_nat_eq — Mathlib

English

For any x ∈ k and any n > 0, there exists z with z^n = x in an algebraically closed field k.

Русский

Для любого x в k и любого n > 0 существует z, такое что z^n = x, если k алгебраически замкнутое.

LaTeX

$$$\exists z, z^n = x$ for given x ∈ k and n > 0.$$

Lean4

theorem exists_pow_nat_eq [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x :=
  by
  have : degree (X ^ n - C x) ≠ 0 := by
    rw [degree_X_pow_sub_C hn x]
    exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
  obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
  use z
  simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
  exact sub_eq_zero.1 hz

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