ker_prodMap — Mathlib

English

Kernel of the product map equals the product of kernels.

Русский

Ядро отображения на произведение равно произведению ядер.

LaTeX

$$$ \\ker (\\\\mathrm{prodMap}(f,g)) = \\ker f \\\\times \\\\ker g $$$

Lean4

@[to_additive ker_prodMap]
theorem ker_prodMap {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') :
    (prodMap f g).ker = f.ker.prod g.ker := by
  rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]

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