le_three_of_sqrt_eq_one

Mathlib.Data.Nat.Sqrt

URI: https://scilib.ai/kg/mathlib#Nat.le_three_of_sqrt_eq_one

English

If sqrt n = 1, then n ≤ 3.

Русский

Пусть sqrt n = 1, тогда n ≤ 3.

LaTeX

$$$\\\\sqrt{n} = 1 \\\\Rightarrow n \\le 3$$$

Lean4

theorem le_three_of_sqrt_eq_one (h : sqrt n = 1) : n ≤ 3 :=
  le_of_lt_succ <| (@sqrt_lt n 2).1 <| by grind

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

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

Разделы

Аффилиация

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