castAddHom_int

Mathlib.Data.Int.Cast.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.castAddHom_int

English

The map Int.castAddHom ℤ equals the identity monoid hom on ℤ.

Русский

В отображении Int.castAddHom ℤ равенство со структурой идентичного гомоморфизма на ℤ.

LaTeX

$$$$ \\mathrm{Int.castAddHom}(\\mathbb{Z}) = \\mathrm{id}_{\\mathbb{Z}}. $$$$

Lean4

@[simp]
theorem castAddHom_int : Int.castAddHom ℤ = AddMonoidHom.id ℤ :=
  ((AddMonoidHom.id ℤ).eq_intCastAddHom rfl).symm

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

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

Разделы

Аффилиация

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