one_div_ne_zero'

Mathlib.Data.Real.ConjExponents

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

English

The reciprocal 1/r is not zero: 1/r ≠ 0.

Русский

Обратная величина 1/r не равна нулю: 1/r ≠ 0.

LaTeX

$$$r^{-1} \neq 0$$$

Lean4

/-- For `r`, instead of `p` -/
theorem one_div_ne_zero' : 1 / r ≠ 0 :=
  ne_of_gt h.one_div_pos'

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

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

Разделы

Аффилиация

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