English
The bilinear smul respects the sum and aligns with the hsum in the target space.
Русский
Двойное умножение сохраняет сумму и согласуется со суммой по целевому пространству.
LaTeX
$$$ (s.smul t).hsum = (of R).symm (s.hsum \cdot (of R) (t.hsum)) $$$
Lean4
theorem smul_hsum {R} {V} [Semiring R] [AddCommMonoid V] [Module R V] (s : SummableFamily Γ R α)
(t : SummableFamily Γ' V β) : (smul s t).hsum = (of R).symm (s.hsum • (of R) (t.hsum)) :=
by
ext g
rw [coeff_smul s t g, HahnModule.coeff_smul, Equiv.symm_apply_apply]
refine
Eq.symm (sum_of_injOn (fun a ↦ a) (fun _ _ _ _ h ↦ h) (fun _ hgh => ?_) (fun gh _ hgh => ?_) fun _ _ => by simp)
· simp_all only [mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, Set.mem_iUnion, and_true]
constructor
· rw [coeff_hsum_eq_sum] at hgh
have h' := Finset.exists_ne_zero_of_sum_ne_zero hgh.1
simpa using h'
· by_contra hi
simp_all
· simp only [Set.image_id', mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, not_and] at hgh
by_cases h : s.hsum.coeff gh.1 = 0
· exact smul_eq_zero_of_left h (t.hsum.coeff gh.2)
· simp_all
