sumInv — Mathlib

English

For a multiset pqr of positive naturals, sumInv(pqr) is the sum of the reciprocals of its elements in rationals.

Русский

Для мультинабора pqr положительных натуральных чисел сумма inv(pqr) равна сумме обратных его элементов в полях раций.

LaTeX

$$$\mathrm{sumInv}(pqr) = \displaystyle\sum_{x \in pqr} x^{-1}$$$

Lean4

/-- `sum_inv pqr` for a `pqr : Multiset ℕ+` is the sum of the inverses
of the elements of `pqr`, as rational number.

The intended argument is a multiset `{p,q,r}` of cardinality `3`. -/
def sumInv (pqr : Multiset ℕ+) : ℚ :=
  Multiset.sum (pqr.map fun (x : ℕ+) => x⁻¹)

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