div_cases

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#Irrational.div_cases

English

If the quotient x/y is irrational, then at least one of x or y is irrational.

Русский

Если частное x/y иррационально, то хотя бы одно из x или y иррационально.

LaTeX

$$$\operatorname{Irr}(x/y) \Rightarrow \operatorname{Irr}(x) \lor \operatorname{Irr}(y)$$$

Lean4

theorem div_cases (h : Irrational (x / y)) : Irrational x ∨ Irrational y :=
  h.mul_cases.imp id of_inv

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

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

Разделы

Аффилиация

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