mk_prod — Mathlib

English

The canonical Noether isomorphism theorem states that there is a canonical isomorphism between G/ker φ and range φ.

Русский

Каноническая теорема Ноетра об изоморфизма утверждает существование канонического изоморфизма между G/ker φ и range φ.

LaTeX

$$$G \\! /\\ker \\phi \\cong \\operatorname{range}(\\phi)$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_prod {G ι : Type*} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} :
    ((Finset.prod s f : G) : G ⧸ N) = Finset.prod s (fun i => (f i : G ⧸ N)) :=
  map_prod (QuotientGroup.mk' N) _ _

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