Theorems · Definition · group theory

AddEquiv.addSubmonoidCongr

{M : Type u_1} → [inst : AddZeroClass M] → {S T : AddSubmonoid M} → S = T → ↥S ≃+ ↥T

Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal.

Defined in

Mathlib.Algebra.Group.Submonoid.Operations

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddZeroClass