exists_eq_mul_self — Mathlib

English

In an algebraically closed field k, every element x is a square: there exists z with x = z^2.

Русский

В алгебраически замкнутом поле каждый элемент является квадратом: существует z, такой что x = z^2.

LaTeX

$$$\exists z, x = z^2$ for any $x \in k$ in [IsAlgClosed k].$$

Lean4

theorem exists_eq_mul_self [IsAlgClosed k] (x : k) : ∃ z, x = z * z :=
  by
  rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩
  exact ⟨z, sq z⟩

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