lift_unique — Mathlib

English

Every monoid homomorphism F : WithOne α →* β is equal to lift of its restriction to α, i.e. F = lift (F.toMulHom.comp coeMulHom).

Русский

Любой моноид-гомоморфизм F : WithOne α →* β равен подъему lift от ограничение F к α: F = lift (F.toMulHom.comp coeMulHom).

LaTeX

$$$F = \mathrm{lift}(F^{\mathrm{toMulHom}} \circ \mathrm{coeMulHom})$$$

Lean4

@[to_additive]
theorem lift_unique (f : WithOne α →* β) : f = lift (f.toMulHom.comp coeMulHom) :=
  (lift.apply_symm_apply f).symm

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