Theorems · Theorem · group theory

MulEquiv.subgroupMap_symm_apply

∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (e : G ≃* G') (H : Subgroup G)
  (g : ↥(Subgroup.map (↑e) H)), (e.subgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

GroupGroup