English
For AddZeroClass M and CommMonoid N, f : Option α →₀ M, b : Option α → M → N, with suitable zero and addition hypotheses, f.prod b equals b none (f none) times f.some.prod (λ a, b (Option.some a)).
Русский
Для AddZeroClass M и CommMonoid N, f : Option α →₀ M, b : Option α → M → N, при подходящих условиях нуля и сложения имеем равенство: f.prod b = b none (f none) · f.some.prod (λ a, b (Option.some a)).
LaTeX
$$$ f.prod\; b = b\; none\; (f\; none) \cdot f.some.prod (\lambda a. b (Option.some a)) $$$
Lean4
@[to_additive]
theorem prod_option_index [AddZeroClass M] [CommMonoid N] (f : Option α →₀ M) (b : Option α → M → N)
(h_zero : ∀ o, b o 0 = 1) (h_add : ∀ o m₁ m₂, b o (m₁ + m₂) = b o m₁ * b o m₂) :
f.prod b = b none (f none) * f.some.prod fun a => b (Option.some a) := by
classical
induction f using induction_linear with
| zero => simp [some_zero, h_zero]
| add f₁ f₂ h₁ h₂ =>
rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
· simp only [h_add, Pi.add_apply, Finsupp.coe_add]
rw [mul_mul_mul_comm]
all_goals simp [h_zero, h_add]
| single a m => cases a <;> simp [h_zero]
