English
Given a distributive law (r+s)•u = r•u + s•u for all r,s,u, we have (x+y)•z = x•z + y•z.
Русский
При наличии линейности распределения (r+s)•u = r•u + s•u выполняется (x+y)•z = x•z + y•z.
LaTeX
$$$(x+y) \\cdot z = x \\cdot z + y \\cdot z$$$
Lean4
theorem add_smul [AddCommMonoid R] [SMulWithZero R V] {x y : HahnSeries Γ R} {z : HahnModule Γ' R V}
(h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u) : (x + y) • z = x • z + y • z :=
by
ext a
have hwf := x.isPWO_support.union y.isPWO_support
rw [coeff_smul_left hwf, HahnSeries.coeff_add', of_symm_add]
· simp_all only [Pi.add_apply, HahnSeries.coeff_add']
rw [coeff_smul_left hwf Set.subset_union_right, coeff_smul_left hwf Set.subset_union_left]
simp only [sum_add_distrib]
· intro b
simp_all only [Set.isPWO_union, HahnSeries.isPWO_support, and_self, HahnSeries.mem_support, HahnSeries.coeff_add,
ne_eq, Set.mem_union]
contrapose!
intro h
rw [h.1, h.2, add_zero]
