zmultiplesHom_symm_apply

Mathlib.Data.Int.Cast.Lemmas

URI: https://scilib.ai/kg/mathlib#zmultiplesHom_symm_apply

English

The inverse of zmultiplesHom β evaluated at f ∈ ℤ →+ β is f(1).

Русский

Обратное zmultiplesHom β при f ∈ ℤ →+ β равно f(1).

LaTeX

$$$$ (zmultiplesHom \\beta).symm f = f(1). $$$$

Lean4

@[simp]
theorem zmultiplesHom_symm_apply (f : ℤ →+ β) : (zmultiplesHom β).symm f = f 1 :=
  rfl

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

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

Разделы

Аффилиация

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