Theorems · Definition · group theory

WithOne.lift

{α : Type u} → {β : Type v} → [inst : Mul α] → [inst_1 : MulOneClass β] → (α →ₙ* β) ≃ (WithOne α →* β)

Lift a semigroup homomorphism f to a bundled monoid homomorphism.

Defined in

Mathlib.Algebra.Group.WithOne.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

MulMulOneClass