Theorems · Definition · group theory

AddEquiv.addSubgroupCongr

{G : Type u_1} → [inst : AddGroup G] → {H K : AddSubgroup G} → H = K → ↥H ≃+ ↥K

Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddGroup