Lean4
/-- The image of a set under a multiplicative homomorphism is a ring homomorphism
with respect to the pointwise operations on sets. -/
noncomputable def imageHom [MulOneClass α] [MulOneClass β] (f : α →* β) : SetSemiring α →+* SetSemiring β
where
toFun s := (image f s.down).up
map_zero' := image_empty _
map_one' := by rw [down_one, image_one, map_one, singleton_one, up_one]
map_add' := image_union _
map_mul' _ _ := image_mul f