English
In a separably closed field k, for any x ∈ k and any n ≥ 1 with n ≠ 0 in k, there exists z ∈ k with z^n = x.
Русский
В сепарабельном замкнутом поле k для любого x ∈ k и любого n≥1 с n ≠ 0 в k существует z ∈ k такое, что z^n = x.
LaTeX
$$$n\neq 0$ in k, $\exists z: z^n = x$$$
Lean4
theorem exists_pow_nat_eq [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero (n : k)] : ∃ z, z ^ n = x :=
by
have hn' : 0 < n :=
Nat.pos_of_ne_zero fun h => by
rw [h, Nat.cast_zero] at hn
exact hn.out rfl
have : degree (X ^ n - C x) ≠ 0 := by
rw [degree_X_pow_sub_C hn' x]
exact (WithBot.coe_lt_coe.2 hn').ne'
by_cases hx : x = 0
· exact ⟨0, by rw [hx, pow_eq_zero_iff hn'.ne']⟩
· obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx
use z
simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def, sub_eq_zero] using hz
