exists_mul_self — Mathlib

English

For any x ∈ ℚ, there exists q ∈ ℚ with q^2 = x if and only if Rat.sqrt(x)² = x.

Русский

Для рационального x существует q ∈ ℚ с q^2 = x тогда и только тогда, когда (Rat.sqrt x)^2 = x.

LaTeX

$$$ \exists q \in \mathbb{Q}, q^2 = x \;\iff\; (\operatorname{Rat.sqrt}(x))^2 = x $$$

Lean4

theorem exists_mul_self (x : ℚ) : (∃ q, q * q = x) ↔ Rat.sqrt x * Rat.sqrt x = x :=
  ⟨fun ⟨n, hn⟩ => by rw [← hn, sqrt_eq, abs_mul_abs_self], fun h => ⟨Rat.sqrt x, h⟩⟩

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