Theorems · Theorem · group theory

Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk

∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (g : ↥s),
  (Subgroup.quotientSubgroupOfEmbeddingOfLE H h) ↑g = ↑((Subgroup.inclusion h) g)

Defined in

Mathlib.GroupTheory.Coset.Basic

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group