Theorems · Definition · commutative algebra

Submodule.mapHom

{R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {A' : Type u_1} →
            [inst_3 : Semiring A'] → [inst_4 : Algebra R A'] → (A →ₐ[R] A') → Submodule R A →+* Submodule R A'

Submonoid.map as a RingHom, when applied to an AlgHom.

Defined in

Mathlib.Algebra.Algebra.Operations

Cited by

3 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringAlgebraSemiringAlgebra