Theorems · Definition · ring theory

RingHom.toAlgebra

{R : Type u_1} → {S : Type u_2} → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → (R →+* S) → Algebra R S

Creating an algebra from a morphism to a commutative semiring. See note [reducible non-instances]. Warning: In general this should not be used if S already has a SMul R S instance, since this creates another SMul R S instance from the supplied RingHom and this will likely create a diamond.

Defined in

Mathlib.Algebra.Algebra.Defs

Cited by

337 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 152 definitions · uses no axioms

Assumes

CommSemiringCommSemiring