quotientMapOfLE_apply_mk — Mathlib

English

For H and h with s ≤ t, and g ∈ H, the map quotientSubgroupOfMapOfLE H h applied to the canonical coset of g equals the canonical coset of g in t.

Русский

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

LaTeX

$$$\\text{If } g \\in H, \\quad \\operatorname{quotientSubgroupOfMapOfLE}\\!\\left(H,h\\right)(\\operatorname{QuotientGroup.mk} g) = \\operatorname{QuotientGroup.mk} g.$$$

Lean4

@[to_additive (attr := simp)]
theorem quotientMapOfLE_apply_mk (h : s ≤ t) (g : α) : quotientMapOfLE h (QuotientGroup.mk g) = QuotientGroup.mk g :=
  rfl

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