map_mk' — Mathlib

English

Variant of map_mk with mk' representing the canonical element in the quotient; the image is the coset of f(x).

Русский

Вариант map_mk с mk' представляющим элемент в фактор-группе; образ — косет f(x).

LaTeX

$$$\\text{map}\\; N\\; M\\; f\\; h\\; (\\mathrm{mk}'\\ _\\ N\\ x) = \\uparrow(f(x)).$$$

Lean4

@[to_additive]
theorem map_mk' (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) : map N M f h (mk' _ x) = ↑(f x) :=
  rfl

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