Theorems · Definition · group theory

MulEquiv.mapSubgroup

{G : Type u_1} → [inst : Group G] → {H : Type u_6} → [inst_1 : Group H] → G ≃* H → Subgroup G ≃o Subgroup H

An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their forward images. See also MulEquiv.comapSubgroup which maps subgroups to their inverse images.

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

11 results in Mathlib

Foundations

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

Assumes

GroupGroup