English
Let Γ be an additively cancellative ordered commutative monoid and R a non-unital non-associative semiring. Then the product of two Hahn series concentrated at a with value r and at b with value s is the Hahn series concentrated at a + b with value r s.
Русский
Пусть Γ — порядочный коммутативный моноид с единицей и дополнительно допускающееся сложение, и R — полугруппа без единицы без ассоциации. Тогда произведение Ганн-по серии, сосредоточенной в a с коэффициентом r, и серии, сосредоточенной в b с коэффициентом s, равно серии, сосредоточенной в a + b с коэффициентом r s.
LaTeX
$$$ \operatorname{single}(a,r) \cdot \operatorname{single}(b,s) = \operatorname{single}(a+b, rs) $$$
Lean4
@[simp]
theorem single_mul_single {a b : Γ} {r s : R} : single a r * single b s = single (a + b) (r * s) :=
by
ext x
by_cases h : x = a + b
· rw [h, coeff_mul_single_add]
simp
· rw [coeff_single_of_ne h, coeff_mul, sum_eq_zero]
simp_rw [mem_addAntidiagonal]
rintro ⟨y, z⟩ ⟨hy, hz, rfl⟩
rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h
exact (h rfl).elim
