ne_zero'

Mathlib.Data.Real.ConjExponents

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

English

In a Holder triple, the third exponent r is nonzero: r ≠ 0.

Русский

В тройке Холдера третий показатель r непустой: r ≠ 0.

LaTeX

$$$r \neq 0$$$

Lean4

/-- For `r`, instead of `p` -/
theorem ne_zero' : r ≠ 0 :=
  h.pos'.ne'

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

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

Разделы

Аффилиация

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