one_div_ne_zero

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#Real.HolderTriple.one_div_ne_zero

English

Let p, q, r be real numbers with p.HolderTriple q r. Then p^{-1} ≠ 0.

Русский

Пусть p, q, r вещественные числа, удовлетворяющие p.HolderTriple q r. Тогда p ≠ 0 (то есть p^{-1} ≠ 0).

LaTeX

$$$ p.HolderTriple q r \rightarrow p^{-1} \neq 0 $$$

Lean4

theorem one_div_ne_zero : 1 / p ≠ 0 :=
  ne_of_gt h.one_div_pos

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

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

Разделы

Аффилиация

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