coe_toAddMonoidHomEquiv

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#AddChar.coe_toAddMonoidHomEquiv

English

AddChar A M is in bijection with MonoidHom A (Additive M).

Русский

AddChar A M и MonoidHom A (Additive M) образуют биекцию.

LaTeX

$$$\mathrm{AddChar}(A,M) \simeq \mathrm{MonoidHom}(A, \mathrm{Additive}(M))$$$

Lean4

@[simp, norm_cast]
theorem coe_toAddMonoidHomEquiv (ψ : AddChar A M) : ⇑(toAddMonoidHomEquiv ψ) = Additive.ofMul ∘ ψ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru