image_coe — Mathlib

English

The image of the quotient map equals the unit element in the quotient of G by N; i.e., the quotient map takes N to 1.

Русский

Образ отображения при фактор-группе совпадает с единицей; отображение отправляет N в 1.

LaTeX

$$$(\\uparrow) : G \\to Q\\;'' N = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem image_coe : ((↑) : G → Q ) '' N = 1 :=
  congr_arg ((↑) : Subgroup Q → Set Q ) <| map_mk'_self N

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