Theorems · Definition · group theory

WithZero.lift

{α : Type u} → {β : Type v} → [inst : Add α] → [inst_1 : AddZeroClass β] → (α →ₙ+ β) ≃ (WithZero α →+ β)

Lift an additive semigroup homomorphism f to a bundled additive 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

AddAddZeroClass