Theorems · Definition · ring theory

Algebra.algebraMapSubmonoid

{R : Type u_1} →
  [inst : CommSemiring R] → (S : Type u_4) → [inst_1 : Semiring S] → [Algebra R S] → Submonoid R → Submonoid S

Explicit characterization of the submonoid map in the case of an algebra. S is made explicit to help with type inference

Defined in

Mathlib.Algebra.Algebra.Basic

Cited by

137 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra