Theorems · Definition · commutative algebra

HomogeneousSubmodule.mk.noConfusion

{ι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 𝒜 ℳ} →
                                            {P : Sort u} →
                                              {toSubmodule : Submodule A M} →
                                                {is_homogeneous' : toSubmodule.IsHomogeneous ℳ} →
                                                  {toSubmodule' : Submodule A M} →
                                                    {is_homogeneous'' : toSubmodule'.IsHomogeneous ℳ} →
                                                      { toSubmodule := toSubmodule,
                                                            is_homogeneous' := is_homogeneous' } =
                                                          { toSubmodule := toSubmodule',
                                                            is_homogeneous' := is_homogeneous'' } →
                                                        (toSubmodule ≍ toSubmodule' → P) → P

Defined in

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Cited by

1 results in Mathlib

Foundations

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