coe_compAddMonoidHom

Mathlib.Algebra.Group.AddChar

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

English

ψ = 0 ⇔ ∀ x, ψ x = 1.

Русский

ψ = 0 ⇔ ∀ x, ψ(x) = 1.

LaTeX

$$$$ \psi = 0 \iff ∀ x \in A, \psi(x) = 1. $$$$

Lean4

@[simp, norm_cast]
theorem coe_compAddMonoidHom (φ : AddChar B M) (f : A →+ B) : φ.compAddMonoidHom f = φ ∘ f :=
  rfl

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

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

Разделы

Аффилиация

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