castRingHom — Mathlib

English

Nat.cast extends to a ring hom from ℕ to α.

Русский

Nat.cast продолжает задавать кольцо-гомоморфизм ℕ → α.

LaTeX

$$$ \operatorname{Nat.cast}(m+n) = \operatorname{Nat.cast}(m) + \operatorname{Nat.cast}(n), \; \operatorname{Nat.cast}(m n) = \operatorname{Nat.cast}(m) \operatorname{Nat.cast}(n), \; \operatorname{Nat.cast}(1) = 1. $$$

Lean4

/-- `Nat.cast : ℕ → α` as a `RingHom` -/
def castRingHom : ℕ →+* α :=
  { castAddMonoidHom α with toFun := Nat.cast, map_one' := cast_one, map_mul' := cast_mul }

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