Theorems · Inductive type · ring theory

AlgHom

(R : Type u) →
  (A : Type v) →
    (B : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Semiring B] → [Algebra R A] → [Algebra R B] → Type (max v w)

Defining the homomorphism in the category R-Alg, denoted A →ₐ[R] B.

Defined in

Mathlib.Algebra.Algebra.Hom

Cited by

3,236 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra