map_mk — Mathlib

English

The induced map on cosets sends the coset of x to the coset of f(x).

Русский

Индуцированное отображение на косетах отправляет косет x на косет f(x).

LaTeX

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

Lean4

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

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