English
Compatibility of mapRange with composition: (mapRange.addMonoidHom f) ∘ (mapRange.addMonoidHom f2) equals mapRange.addMonoidHom with the pointwise composition of f and f2.
Русский
Совместимость mapRange с композициями: (mapRange.addMonoidHom f) ∘ (mapRange.addMonoidHom f2) равен mapRange.addMonoidHom применяемому поперечному композицию f и f2.
LaTeX
$$$\\big(\\mathrm{mapRange}.\\mathrm{addMonoidHom}\\; f\\big) \\circ \\big(\\mathrm{mapRange}.\\mathrm{addMonoidHom}\\; f_2\\big) = \\mathrm{mapRange}.\\mathrm{addMonoidHom}\\; (\\lambda i, f_i \\circ f_{2,i})$$$
Lean4
theorem addMonoidHom_comp (f : ∀ i, β₁ i →+ β₂ i) (f₂ : ∀ i, β i →+ β₁ i) :
(mapRange.addMonoidHom fun i => (f i).comp (f₂ i)) = (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom f₂) :=
by
refine AddMonoidHom.ext <| mapRange_comp (fun i x => f i x) (fun i x => f₂ i x) ?_ ?_ ?_
· intros; apply map_zero
· intros; apply map_zero
· intros; dsimp; simp only [map_zero]
