ker_prod — Mathlib

English

For monoid homs f: G →* M and g: G →* N, the kernel of their product f.prod g is the intersection ker f ∩ ker g.

Русский

Ядро произведения отображений f и g равно пересечению их ядер.

LaTeX

$$$\ker(f \mathrm{.prod} g) = \ker f \cap \ker g$$$

Lean4

@[to_additive ker_prod]
theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
    (f.prod g).ker = f.ker ⊓ g.ker :=
  SetLike.ext fun _ => Prod.mk_eq_one

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