English
Given a ring homomorphism f: R → S, mapping HahnSeries Γ R to HahnSeries Γ S commutes with multiplication, i.e., (x*y).map f = (x.map f) * (y.map f).
Русский
Пусть f: R → S — гомоморфизм колец. Отображение рядов Хана через f сохраняет умножение: (x*y).map f = x.map f * y.map f.
LaTeX
$$$\\forall f:\\, R \\to_{\\!+} S,\\ (x*y).map f = (x.map f) * (y.map f)$$$
Lean4
protected theorem map_mul [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S)
{x y : HahnSeries Γ R} : (x * y).map f = (x.map f : HahnSeries Γ S) * (y.map f) :=
by
ext
simp only [map_coeff, coeff_mul, map_sum, map_mul]
refine Eq.symm (sum_subset (fun gh hgh => ?_) (fun gh hgh hz => ?_))
· simp_all only [mem_addAntidiagonal, mem_support, map_coeff, ne_eq, and_true]
exact ⟨fun h => hgh.1 (map_zero f ▸ congrArg f h), fun h => hgh.2.1 (map_zero f ▸ congrArg f h)⟩
· simp_all only [mem_addAntidiagonal, mem_support, ne_eq, map_coeff, and_true, not_and, not_not]
by_cases h : f (x.coeff gh.1) = 0
· exact mul_eq_zero_of_left h (f (y.coeff gh.2))
· exact mul_eq_zero_of_right (f (x.coeff gh.1)) (hz h)
