prod_map_comap_prod' — Mathlib

English

For f : M →* N and g : M' →* N' and submonoids S ⊆ N, S' ⊆ N', we have (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g).

Русский

Для f : M →* N и g : M' →* N' и подмонойдов S ⊆ N, S' ⊆ N' выполняется (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g).

LaTeX

$$$$ (S.{prod}S').{comap}(\\mathrm{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*} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N')
    (S : Submonoid N) (S' : Submonoid 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 _ _

Похожие утверждения