compAddMonoidHom_apply

Mathlib.Algebra.Group.AddChar

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem compAddMonoidHom_apply (ψ : AddChar B M) (f : A →+ B) (a : A) : ψ.compAddMonoidHom f a = ψ (f a) :=
  rfl

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

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

Разделы

Аффилиация

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