coe_toMonoidHomEquiv — Mathlib

English

The equivalence sends a character to its corresponding monoid homomorphism and vice versa.

Русский

Эквиваленция переводит характер в соответствующий моноид-гомоморфизм и обратно.

LaTeX

$$$toMonoidHomEquiv(\varphi) = \text{the corresponding MonoidHom}$; its inverse maps a MonoidHom back to the AddChar.$$

Lean4

@[simp, norm_cast]
theorem coe_toMonoidHomEquiv (ψ : AddChar A M) : ⇑(toMonoidHomEquiv ψ) = ψ ∘ Multiplicative.toAdd :=
  rfl

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