English
Let f: M → N and g: M' → N' be semigroup homs, S ≤ N and S' ≤ N'. Then the comap of the product map equals the product of comaps: (S × S').comap (prodMap f g) = (S.comap f) × (S'.comap g).
Русский
Пусть f: M → N и g: M' → N' — полугомомы; тогда поразрядное отображение произведения равно произведению прообразов: (S × S').comap (prodMap f g) = (S.comap f) × (S'.comap g).
LaTeX
$$$ (S \ prod S').comap (prodMap\ f\ g) = (S.comap f) \prod (S'.comap g) $$$
Lean4
@[to_additive prod_map_comap_prod']
theorem prod_map_comap_prod' {M' : Type*} {N' : Type*} [Mul M'] [Mul N'] (f : M →ₙ* N) (g : M' →ₙ* N')
(S : Subsemigroup N) (S' : Subsemigroup N') : (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g) :=
SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _
