Theorems · Definition · group theory

AddEquiv.toAddMonoidHom

{M : Type u_4} → {N : Type u_5} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N

Extract the forward direction of an additive equivalence as an addition-preserving function.

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

101 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 82 definitions · uses Quot.sound

Assumes

AddZeroClassAddZeroClass