Theorems · Definition · group theory

MulEquiv.toMonoidHom

{M : Type u_4} → {N : Type u_5} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N

Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

126 results in Mathlib

Foundations

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

Assumes

MulOneClassMulOneClass