quotientSubgroupOfMapOfLE — Mathlib

English

If s ≤ t, there is a canonical map from H/(s.subgroupOf H) to H/(t.subgroupOf H).

Русский

Если s ≤ t, существует каноничное отображение из H/(s.subgroupOf H) в H/(t.subgroupOf H).

LaTeX

$$$\\text{If } s \\leq t, \\quad H \\!\\! / \\!\\! (s\\text{-subgroupOf } H) \\to H \\!\\! / \\!\\! (t\\text{-subgroupOf } H).$$$

Lean4

/-- If `s ≤ t`, then there is a map `H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H`. -/
@[to_additive /-- If `s ≤ t`, then there is a map `H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H`. -/
    ]
def quotientSubgroupOfMapOfLE (H : Subgroup α) (h : s ≤ t) : H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H :=
  Quotient.map' id fun a b => by
    simp_rw [leftRel_eq]
    apply h

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