toAddMonoidHom_apply

Mathlib.Algebra.Group.AddChar

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

English

Symmetric application preserves evaluation under Multiplicative view.

Русский

При симметрическом применении сохраняется вычисление в мультипликативном виде.

LaTeX

$$toMonoidHomEquiv.symm φ a = φ(a).toMul$$

Lean4

@[simp]
theorem toAddMonoidHom_apply (ψ : AddChar A M) (a : A) : ψ.toAddMonoidHom a = Additive.ofMul (ψ a) :=
  rfl

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

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

Разделы

Аффилиация

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