quotientSubgroupOfEmbeddingOfLE_apply_mk

English

Let H be a subgroup of α and s ≤ t be subgroups of α with g ∈ s. The natural map induced by inclusion sends the coset of g modulo s to the coset of g modulo t.

Русский

Пусть H ≤ α и s ≤ t — подгруппы α, и пусть g ∈ s. Естественный отображение, индуцированное включением, переводит косет в отношении s в косет в отношении t.

LaTeX

$$$\\text{If } H \\leq \\alpha \\text{ and } s \\leq t, \\quad [g]_{s} \\mapsto [g]_{t} = [\\iota_h(g)]_{t}$, where $g \\in s$ and $\\iota_h: s \\hookrightarrow t$ is the inclusion.$$

Lean4

@[to_additive (attr := simp)]
theorem quotientSubgroupOfEmbeddingOfLE_apply_mk (H : Subgroup α) (h : s ≤ t) (g : s) :
    quotientSubgroupOfEmbeddingOfLE H h (QuotientGroup.mk g) = QuotientGroup.mk (inclusion h g) :=
  rfl

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