Theorems · Inductive type · commutative algebra

GradedRingHom

{ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [Semiring A] → [Semiring B] → [SetLike σ A] → [SetLike τ B] → (ι → σ) → (ι → τ) → Type (max u_2 u_3)

Bundled graded (semi)ring homomorphisms. Use GradedRingHom for the namespace and other identifiers, and 𝒜 →+*ᵍ ℬ for the notation.

Defined in

Mathlib.RingTheory.GradedAlgebra.RingHom

Cited by

91 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SemiringSemiringSetLikeSetLike