sub_one_mul_conj

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderConjugate.sub_one_mul_conj

English

If p and q are Holder conjugates, then (p − 1) · q = p.

Русский

Если p и q — сопряжённые Холдеру, то (p − 1) · q = p.

LaTeX

$$(p - 1) * q = p$$

Lean4

theorem sub_one_mul_conj : (p - 1) * q = p :=
  mul_comm q (p - 1) ▸ (eq_div_iff h.sub_one_ne_zero).1 h.conjugate_eq

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

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

Разделы

Аффилиация

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