toNatAlgHom — Mathlib

English

There is a canonical way to view a RingHom as a ℕ-algebra homomorphism; f : R →+* S gives f : R →ₐ[ℕ] S.

Русский

Существет канонический способ рассматривать RingHom как ℕ-алгебра-гомоморфизм: f : R →+* S даёт f : R →ₐ[ℕ] S.

LaTeX

$$$$ f \text{ as } R \to S \text{ viewed as } \mathbb{N}\text{-algebra homomorphism}. $$$$

Lean4

/-- Reinterpret a `RingHom` as an `ℕ`-algebra homomorphism. -/
def toNatAlgHom [Semiring R] [Semiring S] (f : R →+* S) : R →ₐ[ℕ] S :=
  { f with
    toFun := f
    commutes' := fun n => by simp }

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