Theorems · Definition · commutative algebra

HomogeneousSubmodule.noConfusion

{P : Sort u} →
  {ιA : Type u_1} →
    {ιM : Type u_2} →
      {σA : Type u_3} →
        {σM : Type u_4} →
          {A : Type u_5} →
            {M : Type u_6} →
              {inst : Semiring A} →
                {inst_1 : AddCommMonoid M} →
                  {inst_2 : Module A M} →
                    {𝒜 : ιA → σA} →
                      {ℳ : ιM → σM} →
                        {inst_3 : DecidableEq ιA} →
                          {inst_4 : AddMonoid ιA} →
                            {inst_5 : SetLike σA A} →
                              {inst_6 : AddSubmonoidClass σA A} →
                                {inst_7 : GradedRing 𝒜} →
                                  {inst_8 : DecidableEq ιM} →
                                    {inst_9 : SetLike σM M} →
                                      {inst_10 : AddSubmonoidClass σM M} →
                                        {inst_11 : DirectSum.Decomposition ℳ} →
                                          {inst_12 : VAdd ιA ιM} →
                                            {inst_13 : SetLike.GradedSMul 𝒜 ℳ} →
                                              {t : HomogeneousSubmodule 𝒜 ℳ} →
                                                {ιA' : Type u_1} →
                                                  {ιM' : Type u_2} →
                                                    {σA' : Type u_3} →
                                                      {σM' : Type u_4} →
                                                        {A' : Type u_5} →
                                                          {M' : Type u_6} →
                                                            {inst' : Semiring A'} →
                                                              {inst'_1 : AddCommMonoid M'} →
                                                                {inst'_2 : Module A' M'} →
                                                                  {𝒜' : ιA' → σA'} →
                                                                    {ℳ' : ιM' → σM'} →
                                                                      {inst'_3 : DecidableEq ιA'} →
                                                                        {inst'_4 : AddMonoid ιA'} →
                                                                          {inst'_5 : SetLike σA' A'} →
                                                                            {inst'_6 : AddSubmonoidClass σA' A'} →
                                                                              {inst'_7 : GradedRing 𝒜'} →
                                                                                {inst'_8 : DecidableEq ιM'} →
                                                                                  {inst'_9 : SetLike σM' M'} →
                                                                                    {inst'_10 :
                                                                                        AddSubmonoidClass σM' M'} →
                                                                                      {inst'_11 :
                                                                                          DirectSum.Decomposition ℳ'} →
                                                                                        {inst'_12 : VAdd ιA' ιM'} →
                                                                                          {inst'_13 :
                                                                                              SetLike.GradedSMul 𝒜'
                                                                                                ℳ'} →
                                                                                            {t' :
                                                                                                HomogeneousSubmodule 𝒜'
                                                                                                  ℳ'} →
                                                                                              ιA = ιA' →
                                                                                                ιM = ιM' →
                                                                                                  σA = σA' →
                                                                                                    σM = σM' → ⋯

Defined in

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Cited by

0 results in Mathlib

Foundations

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