mker_prod_map — Mathlib

English

The kernel of the product map equals the product of kernels: mker (f.prodMap g) = (mker f).prod (mker g).

Русский

Ядро произведения отображений равно произведению ядер: mker(f.prodMap g) = (mker f).prod (mker g).

LaTeX

$$$$ \\mathrm{mker}(\\mathrm{f}.{prodMap}\\; g) = (\\mathrm{mker}\\; f).{prod}(\\mathrm{mker}\\; g) $$$$

Lean4

@[to_additive mker_prod_map]
theorem mker_prod_map {M' : Type*} {N' : Type*} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') :
    mker (prodMap f g) = (mker f).prod (mker g) := by
  rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_bot]

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