exists_eq_mul_self — Mathlib

English

If 2 ≠ 0 in a separably closed field k, every element is a square: ∃ z, x = z^2.

Русский

Если 2 не нуль в поле k, сепарабельное замкнутое, то каждый элемент является квадратом: ∃ z, x = z^2.

LaTeX

$$$2 \neq 0 \Rightarrow ∃ z:\ x = z^2$$$

Lean4

theorem exists_eq_mul_self [IsSepClosed k] (x : k) [h2 : NeZero (2 : k)] : ∃ z, x = z * z :=
  by
  rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩
  exact ⟨z, sq z⟩

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