Theorems · Definition · ring theory

GradedAlgHom.id

(R : Type u_1) →
  {A : Type u_6} →
    {ι : Type u_10} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : DecidableEq ι] →
              [inst_4 : AddMonoid ι] → (𝒜 : ι → Submodule R A) → [inst_5 : GradedAlgebra 𝒜] → 𝒜 →ₐᵍ[R] 𝒜

Identity map as a GradedAlgHom.

Defined in

Mathlib.RingTheory.GradedAlgebra.AlgHom

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraDecidableEqAddMonoidGradedAlgebra