Theorems · Definition · ring theory

Algebra.compHom

{R : Type u} →
  {S : Type v} →
    (A : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] → [inst_2 : Semiring A] → [Algebra R A] → (S →+* R) → Algebra S A

Compose an Algebra with a RingHom, with action f s • m. This is the algebra version of Module.compHom.

Defined in

Mathlib.Algebra.Algebra.Defs

Cited by

10 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringSemiringAlgebra