English
For Hahn series acting on a Hahn module, smul distributes over addition in the module: x • (y + z) = x • y + x • z.
Русский
Для Ханновой серии, действующей на Hahn-модуль, умножение на сумму распределяется по сложению модуля: x • (y + z) = x • y + x • z.
LaTeX
$$$ x \cdot (y + z) = x \cdot y + x \cdot z $$$
Lean4
theorem smul_add [Zero R] [DistribSMul R V] (x : HahnSeries Γ R) (y z : HahnModule Γ' R V) :
x • (y + z) = x • y + x • z := by
ext k
have hwf := ((of R).symm y).isPWO_support.union ((of R).symm z).isPWO_support
rw [coeff_smul_right hwf, of_symm_add]
· simp_all only [HahnSeries.coeff_add', Pi.add_apply, of_symm_add]
rw [coeff_smul_right hwf Set.subset_union_right, coeff_smul_right hwf Set.subset_union_left]
simp_all [sum_add_distrib]
· intro b
simp_all only [Set.isPWO_union, HahnSeries.isPWO_support, and_self, of_symm_add, HahnSeries.coeff_add',
Pi.add_apply, ne_eq, Set.mem_union, HahnSeries.mem_support]
contrapose!
intro h
rw [h.1, h.2, add_zero]
