English
In a semiring R and an R-module M, f : Option α →₀ R, b : Option α → M, we have sum over o of (r • b(o)) equals f.none • b(none) plus f.some.sum over a of (r • b(Some a)).
Русский
В полукольце R и модуле M над R имеем: сумма по o от r • b(o) равна f.none • b(none) плюс сумма по a от f.some of r • b(Some a).
LaTeX
$$$ f.sum (\lambda o r. r \cdot b(o)) = f.none \cdot b(none) + f.some.sum(\lambda a r. r \cdot b(Option.some a)) $$$
Lean4
theorem sum_option_index_smul [Semiring R] [AddCommMonoid M] [Module R M] (f : Option α →₀ R) (b : Option α → M) :
(f.sum fun o r => r • b o) = f none • b none + f.some.sum fun a r => r • b (Option.some a) :=
f.sum_option_index _ (fun _ => zero_smul _ _) fun _ _ _ => add_smul _ _ _
