zpowersMulHom_symm_apply — Mathlib

English

The inverse map of zpowersMulHom sends a monoid hom f to its value at 1: (zpowersMulHom α).symm f = f(1).

Русский

Обратная карта zpowersMulHom отправляет моноид-гомоморфизм f в его значение в единице: (zpowersMulHom α).symm f = f(1).

LaTeX

$$$ (zpowersMulHom\\alpha).symm\\ f = f(1) $$$

Lean4

@[simp]
theorem zpowersMulHom_symm_apply (f : Multiplicative ℤ →* α) : (zpowersMulHom α).symm f = f (ofAdd 1) :=
  rfl

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