sqrt_mul_sqrt_lt_succ

Mathlib.Data.Nat.Sqrt

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

English

There are no t with t^2 = n when m^2 < n < (m+1)^2.

Русский

Между квадратами m^2 и (m+1)^2 не существует числа t, такого что t^2 = n.

LaTeX

$$$ m^2 < n \\Rightarrow n < (m+1)^2 \\Rightarrow \\neg \\exists t\\, t^2 = n $$$

Lean4

theorem sqrt_mul_sqrt_lt_succ (n : ℕ) : sqrt n * sqrt n < n + 1 :=
  Nat.lt_succ_iff.mpr (sqrt_le _)

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

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

Разделы

Аффилиация

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