Theorems · Definition · commutative algebra

HomogeneousSubsemiring.noConfusion

{P : Sort u} →
  {ι : Type u_1} →
    {σ : Type u_2} →
      {A : Type u_3} →
        {inst : AddMonoid ι} →
          {inst_1 : Semiring A} →
            {inst_2 : SetLike σ A} →
              {inst_3 : AddSubmonoidClass σ A} →
                {𝒜 : ι → σ} →
                  {inst_4 : DecidableEq ι} →
                    {inst_5 : GradedRing 𝒜} →
                      {t : HomogeneousSubsemiring 𝒜} →
                        {ι' : Type u_1} →
                          {σ' : Type u_2} →
                            {A' : Type u_3} →
                              {inst' : AddMonoid ι'} →
                                {inst'_1 : Semiring A'} →
                                  {inst'_2 : SetLike σ' A'} →
                                    {inst'_3 : AddSubmonoidClass σ' A'} →
                                      {𝒜' : ι' → σ'} →
                                        {inst'_4 : DecidableEq ι'} →
                                          {inst'_5 : GradedRing 𝒜'} →
                                            {t' : HomogeneousSubsemiring 𝒜'} →
                                              ι = ι' →
                                                σ = σ' →
                                                  A = A' →
                                                    inst ≍ inst' →
                                                      inst_1 ≍ inst'_1 →
                                                        inst_2 ≍ inst'_2 →
                                                          inst_3 ≍ inst'_3 →
                                                            𝒜 ≍ 𝒜' →
                                                              inst_4 ≍ inst'_4 →
                                                                inst_5 ≍ inst'_5 →
                                                                  t ≍ t' → HomogeneousSubsemiring.noConfusionType P t t'

Defined in

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Cited by

0 results in Mathlib

Foundations

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