uniqueRingHom — Mathlib

English

There exists a unique ring homomorphism from ℕ to every NonAssocSemiring R.

Русский

Существует единственный кольцевой гомоморфизм из ℕ в любой неассоциативный полукольцо R.

LaTeX

$$$$ \exists! f: \mathbb{N} \to+* R \quad \text{ such that } f \text{ is a ring hom.} $$$$

Lean4

/-- We don't use `RingHomClass` here, since that might cause type-class slowdown for
`Subsingleton`. -/
instance uniqueRingHom {R : Type*} [NonAssocSemiring R] : Unique (ℕ →+* R)
    where
  default := Nat.castRingHom R
  uniq := RingHom.eq_natCast'

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