sumInv_pqr

Mathlib.NumberTheory.ADEInequality

URI: https://scilib.ai/kg/mathlib#ADEInequality.sumInv_pqr

← MathLib Explorer

English

For p,q,r in N+, the sumInv of {p,q,r} equals p^{-1}+q^{-1}+r^{-1}.

Русский

Для p,q,r ∈ N+ сумма inv({p,q,r}) равна p^{-1}+q^{-1}+r^{-1}.

LaTeX

$$$\mathrm{sumInv}\{p,q,r\} = p^{-1} + q^{-1} + r^{-1}$$$

Lean4

theorem sumInv_pqr (p q r : ℕ+) : sumInv { p, q, r } = (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ := by
  simp only [sumInv, insert_eq_cons, add_assoc, map_cons, sum_cons, map_singleton, sum_singleton]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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