English
There is a universal property: lift' induces an equivalence between α →* β and WithZero α →*₀ β.
Русский
Существует универсальное свойство: lift' задаёт эквивалентность между отображениями α →* β и WithZero α →*₀ β.
LaTeX
$$$\\text{lift'} : (\\alpha \\toess) \\simeq (WithZero \\alpha \\to*_{0} \\beta)$$$
Lean4
/-- The (multiplicative) universal property of `WithZero`. -/
@[simps! symm_apply_apply]
nonrec def lift' : (α →* β) ≃ (WithZero α →*₀ β)
where
toFun
f :=
{ toFun := recZeroCoe 0 f
map_zero' := rfl
map_one' := by simp
map_mul' := fun
| 0, _ => (zero_mul _).symm
| (_ : α), 0 => (mul_zero _).symm
| (_ : α), (_ : α) => map_mul f _ _ }
invFun F := F.toMonoidHom.comp coeMonoidHom
