sq_eq_one_of_sq_le_three

Mathlib.Data.Int.Order.Units

URI: https://scilib.ai/kg/mathlib#Int.sq_eq_one_of_sq_le_three

← MathLib Explorer

English

If x^2 ≤ 3 and x ≠ 0 in ℤ, then x^2 = 1.

Русский

Если x^2 ≤ 3 и x ≠ 0 в ℤ, то x^2 = 1.

LaTeX

$$$\forall x \in \mathbb{Z}, x^{2} \le 3 \to (x \neq 0 \to x^{2} = 1).$$$

Lean4

theorem sq_eq_one_of_sq_le_three {x : ℤ} (h1 : x ^ 2 ≤ 3) (h2 : x ≠ 0) : x ^ 2 = 1 :=
  sq_eq_one_of_sq_lt_four (lt_of_le_of_lt h1 (lt_add_one (3 : ℤ))) h2

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru