quotientSubgroupOfEmbeddingOfLE — Mathlib

English

If s ≤ t, there is an embedding s ⧸ H.subgroupOf s → t ⧸ H.subgroupOf t.

Русский

Если s ≤ t, существует вложение s ⧸ H.subgroupOf s ⊆ t ⧸ H.subgroupOf t.

LaTeX

$$$s \le t \Rightarrow s / H^{\mathrm{subgroupOf} s} \hookrightarrow t / H^{\mathrm{subgroupOf} t}$$$

Lean4

/-- If `s ≤ t`, then there is an embedding `s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t`. -/
@[to_additive /-- If `s ≤ t`, there is an embedding `s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t`. -/
    ]
def quotientSubgroupOfEmbeddingOfLE (H : Subgroup α) (h : s ≤ t) : s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t
    where
  toFun :=
    Quotient.map' (inclusion h) fun a b => by
      simp_rw [leftRel_eq]
      exact id
  inj' :=
    Quotient.ind₂' <| by
      intro a b h
      simpa only [Quotient.map'_mk'', QuotientGroup.eq] using h

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