irrational_sqrt

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#Nat.Prime.irrational_sqrt

English

For a prime p, sqrt(p) is irrational.

Русский

Для простого p корень sqrt(p) иррационален.

LaTeX

$$$\mathrm{Irrational}(\sqrt{p})$ для любого простого p$$

Lean4

theorem irrational_sqrt {p : ℕ} (hp : Nat.Prime p) : Irrational (√p) :=
  irrational_sqrt_natCast_iff.mpr hp.not_isSquare

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

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

Разделы

Аффилиация

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