Theorems · Theorem · commutative algebra

HomogeneousSubmodule.mk.inj

∀ {ι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 𝒜 ℳ}
  {toSubmodule : Submodule A M} {is_homogeneous' : toSubmodule.IsHomogeneous ℳ} {toSubmodule_1 : Submodule A M}
  {is_homogeneous'_1 : toSubmodule_1.IsHomogeneous ℳ},
  { toSubmodule := toSubmodule, is_homogeneous' := is_homogeneous' } =
      { toSubmodule := toSubmodule_1, is_homogeneous' := is_homogeneous'_1 } →
    toSubmodule = toSubmodule_1

Defined in

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Cited by

1 results in Mathlib

Foundations

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