English
A version of ENat.map for RingHom; ENat.map lifts a ℕ →+* S to ENat(WithTop S) compatibly with ring structure.
Русский
Версия ENat.map для RingHom; ENat.map поднимает ℕ →+* S к ENat(WithTop S) совместимо с кольцевой структурой.
LaTeX
$$$$ \\text{RingHom.ENatMap}(f)(n) = \\mathrm{ENat.map}(f)(n) \\quad (n \\in \\mathbb{N}^∞) $$$$
Lean4
/-- A version of `ENat.map` for `RingHom`s. -/
@[simps -fullyApplied]
protected def _root_.RingHom.ENatMap {S : Type*} [CommSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S]
[DecidableEq S] [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective f) : ℕ∞ →+* WithTop S :=
{ MonoidWithZeroHom.ENatMap f.toMonoidWithZeroHom hf, f.toAddMonoidHom.ENatMap with }
