coe_toAddMonoidHom

Mathlib.Algebra.Group.AddChar

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

English

Properties of the equivalence with respect to zero and one coincide with Monoid structures.

Русский

Свойства эквивалентности относительно нуля и единицы согласованы с моноидной структурой.

LaTeX

$$toMonoidHomEquiv 0 = 0 and toMonoidHomEquiv 1 = 1, etc.$$

Lean4

@[simp]
theorem coe_toAddMonoidHom (ψ : AddChar A M) : ⇑ψ.toAddMonoidHom = Additive.ofMul ∘ ψ :=
  rfl

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

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

Разделы

Аффилиация

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