inv_inv_add_inv

Mathlib.Data.Real.ConjExponents

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

English

From HolderTriple, we have (p^{-1} + q^{-1})^{-1} = r.

Русский

Из тройки Холдера следует, что (p^{-1} + q^{-1})^{-1} = r.

LaTeX

$$$\bigl(p^{-1} + q^{-1}\bigr)^{-1} = r$$$

Lean4

theorem inv_inv_add_inv : (p⁻¹ + q⁻¹)⁻¹ = r := by exact_mod_cast h.coe.inv_inv_add_inv

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

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

Разделы

Аффилиация

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