castAddHom — Mathlib

English

The map from integers to α given by casting is an additive monoid hom, i.e., it preserves zero and addition.

Русский

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

LaTeX

$$$\text{castAddHom}(\alpha): \mathbb{Z} \to^+ \alpha$ is defined by $\text{toFun}(z) = z$ (cast to $\alpha$).$$

Lean4

/-- `coe : ℤ → α` as an `AddMonoidHom`. -/
def castAddHom (α : Type*) [AddGroupWithOne α] : ℤ →+ α
    where
  toFun := Int.cast
  map_zero' := cast_zero
  map_add' := cast_add

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