tsum_const_smul — Mathlib

English

For any R with a scalar action on ENNReal and IsScalarTower, ∑' i, a • f(i) = a • ∑' i, f(i).

Русский

Для кольца действий с ENNReal и т. д. сохраняется линейность суммы: ∑' i, a•f(i) = a•∑' i, f(i).

LaTeX

$$$\sum'_{i \in \alpha} a \cdot f(i) = a \cdot \sum'_{i \in \alpha} f(i)$$$

Lean4

protected theorem tsum_const_smul {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (a : R) :
    ∑' i, a • f i = a • ∑' i, f i := by simpa only [smul_one_mul] using @ENNReal.tsum_mul_left _ (a • (1 : ℝ≥0∞)) _

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