liftMonoid_coe_addMonoidHom — Mathlib

English

The underlying AddMonoidHom of liftMonoid f coincides with the corresponding coercion; i.e., the coe of liftMonoid f equals lift f.

Русский

Базовая функция AddMonoidHom liftMonoid f совпадает с соответствующей коэрцией; т. е. коэр liftMonoid f равен lift f.

LaTeX

$$$\uparrow(\mathrm{liftMonoid} f) = \mathrm{lift} f$$$

Lean4

@[simp]
theorem liftMonoid_coe_addMonoidHom (f : α →* R) : ↑(liftMonoid f) = lift f :=
  rfl

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