quotientSubgroupOfMapOfLE_apply_mk

English

For H, h with s ≤ t and g ∈ H, the map quotientSubgroupOfMapOfLE H h sends the coset of g to the same coset, i.e., it preserves representatives.

Русский

Для H, h с s ≤ t и g ∈ H отображение quotientSubgroupOfMapOfLE H h отправляет косет g в тот же косет, т.е. сохраняет представителя.

LaTeX

$$$\\text{If } h: s \\le t, \\quad (\\operatorname{QuotientGroup.mk} g) \\; \\mapsto \\; \\operatorname{QuotientGroup.mk} g,$$$

Lean4

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

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