mul_eq_add

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#Real.HolderConjugate.mul_eq_add

English

If p and q are Holder conjugates, then p q = p + q.

Русский

Если p и q сопряжены Холдером, то p q = p + q.

LaTeX

$$$p q = p + q$$$

Lean4

theorem mul_eq_add : p * q = p + q := by simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj

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

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

Разделы

Аффилиация

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