coe_castRingHom

Mathlib.Data.Int.Cast.Lemmas

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

English

The map from integers to α given by the cast is an additive monoid hom.

Русский

Отображение целых чисел в α через приведение образует гомоморфизм аддитивной моноиды.

LaTeX

$$$\text{Int.castAddHom}(\alpha): \mathbb{Z} \to^+ \alpha$ with $\mathrm{toFun}(z) = z$ in $\alpha$.$$

Lean4

@[simp]
theorem coe_castRingHom : ⇑(castRingHom α) = fun x : ℤ ↦ (x : α) :=
  rfl

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

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

Разделы

Аффилиация

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