lift'_unique — Mathlib

English

Every monoid-with-zero hom f : WithZero α →*₀ β is determined by its underlying monoid hom part; namely, f = lift'( f.toMonoidHom ∘ coeMonoidHom ).

Русский

Любой гомоморфизм WithZero α →*₀ β определяется своей моноидной частью; то есть f = lift'( f.toMonoidHom ∘ coeMonoidHom ).

LaTeX

$$$ f = \\mathrm{lift}'\\bigl( f^{\\mathrm{toMonoidHom}} \\circ \\mathrm{coeMonoidHom} \\bigr). $$$

Lean4

theorem lift'_unique (f : WithZero α →*₀ β) : f = lift' (f.toMonoidHom.comp coeMonoidHom) :=
  (lift'.apply_symm_apply f).symm

Похожие утверждения