Documentation

Mathlib.RingTheory.Ideal.Operations

More operations on modules and ideals #

instance Submodule.hasSMul' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
SMul (Ideal R) (Submodule R M)
Equations
theorem Ideal.smul_eq_mul {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) :
I J = I * J

This duplicates the global smul_eq_mul, but doesn't have to unfold anywhere near as much to apply.

def Module.annihilator (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :

Module.annihilator R M is the ideal of all elements r : R such that r • M = 0.

Equations
Instances For
    theorem Module.mem_annihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} :
    r Module.annihilator R M ∀ (m : M), r m = 0
    theorem LinearEquiv.annihilator_eq {R : Type u} {M : Type v} {M' : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') :
    @[reducible, inline]
    abbrev Submodule.annihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :

    N.annihilator is the ideal of all elements r : R such that r • N = 0.

    Equations
    Instances For
      theorem Submodule.annihilator_top {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
      .annihilator = Module.annihilator R M
      theorem Submodule.mem_annihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {r : R} :
      r N.annihilator nN, r n = 0
      theorem Submodule.mem_annihilator' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {r : R} :
      r N.annihilator N Submodule.comap (r LinearMap.id)
      theorem Submodule.mem_annihilator_span {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set M) (r : R) :
      r (Submodule.span R s).annihilator ∀ (n : s), r n = 0
      theorem Submodule.mem_annihilator_span_singleton {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (g : M) (r : R) :
      r (Submodule.span R {g}).annihilator r g = 0
      theorem Submodule.annihilator_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
      .annihilator =
      theorem Submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :
      N.annihilator = N =
      theorem Submodule.annihilator_mono {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {P : Submodule R M} (h : N P) :
      P.annihilator N.annihilator
      theorem Submodule.annihilator_iSup {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (ι : Sort w) (f : ιSubmodule R M) :
      (⨆ (i : ι), f i).annihilator = ⨅ (i : ι), (f i).annihilator
      theorem Submodule.smul_mem_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {r : R} {n : M} (hr : r I) (hn : n N) :
      r n I N
      theorem Submodule.smul_le {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {P : Submodule R M} :
      I N P rI, nN, r n P
      @[simp]
      theorem Submodule.coe_set_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} :
      I N = I N
      theorem Submodule.smul_induction_on {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {p : MProp} {x : M} (H : x I N) (smul : rI, nN, p (r n)) (add : ∀ (x y : M), p xp yp (x + y)) :
      p x
      theorem Submodule.smul_induction_on' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {x : M} (hx : x I N) {p : (x : M) → x I NProp} (smul : ∀ (r : R) (hr : r I) (n : M) (hn : n N), p (r n) ) (add : ∀ (x : M) (hx : x I N) (y : M) (hy : y I N), p x hxp y hyp (x + y) ) :
      p x hx

      Dependent version of Submodule.smul_induction_on.

      theorem Submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {m : M} {x : M} :
      x I Submodule.span R {m} yI, y m = x
      theorem Submodule.smul_le_right {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} :
      I N N
      theorem Submodule.smul_mono {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {J : Ideal R} {N : Submodule R M} {P : Submodule R M} (hij : I J) (hnp : N P) :
      I N J P
      theorem Submodule.smul_mono_left {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {J : Ideal R} {N : Submodule R M} (h : I J) :
      I N J N
      instance Submodule.instCovariantClassIdealHSMulLe {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
      CovariantClass (Ideal R) (Submodule R M) HSMul.hSMul LE.le
      Equations
      • =
      @[deprecated smul_mono_right]
      theorem Submodule.smul_mono_right {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {P : Submodule R M} (h : N P) :
      I N I P
      theorem Submodule.map_le_smul_top {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (f : R →ₗ[R] M) :
      @[simp]
      theorem Submodule.annihilator_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :
      N.annihilator N =
      @[simp]
      theorem Submodule.smul_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) :
      @[simp]
      theorem Submodule.bot_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :
      @[simp]
      theorem Submodule.top_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :
      N = N
      theorem Submodule.smul_sup {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) (P : Submodule R M) :
      I (N P) = I N I P
      theorem Submodule.sup_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (J : Ideal R) (N : Submodule R M) :
      (I J) N = I N J N
      theorem Submodule.smul_assoc {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (J : Ideal R) (N : Submodule R M) :
      (I J) N = I J N
      @[deprecated smul_inf_le]
      theorem Submodule.smul_inf_le {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (M₁ : Submodule R M) (M₂ : Submodule R M) :
      I (M₁ M₂) I M₁ I M₂
      theorem Submodule.smul_iSup {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} {I : Ideal R} {t : ιSubmodule R M} :
      I iSup t = ⨆ (i : ι), I t i
      @[deprecated smul_iInf_le]
      theorem Submodule.smul_iInf_le {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} {I : Ideal R} {t : ιSubmodule R M} :
      I iInf t ⨅ (i : ι), I t i
      theorem Submodule.span_smul_span {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Set R) (T : Set M) :
      Ideal.span S Submodule.span R T = Submodule.span R (sS, tT, {s t})
      theorem Submodule.ideal_span_singleton_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) :
      Ideal.span {r} N = r N
      theorem Submodule.mem_of_span_top_of_smul_mem {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ) (x : M) (H : ∀ (r : s), r x M') :
      x M'
      theorem Submodule.mem_of_span_eq_top_of_smul_pow_mem {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ) (x : M) (H : ∀ (r : s), ∃ (n : ), r ^ n x M') :
      x M'

      Given s, a generating set of R, to check that an x : M falls in a submodule M' of x, we only need to show that r ^ n • x ∈ M' for some n for each r : s.

      @[simp]
      theorem Submodule.map_smul'' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) {M' : Type w} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') :
      @[simp]
      theorem Submodule.map_pointwise_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (r : R) (N : Submodule R M) (f : M →ₗ[R] M') :
      theorem Submodule.mem_smul_span {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {s : Set M} {x : M} :
      x I Submodule.span R s x Submodule.span R (aI, bs, {a b})
      theorem Submodule.mem_ideal_smul_span_iff_exists_sum {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) {ι : Type u_4} (f : ιM) (x : M) :
      x I Submodule.span R (Set.range f) ∃ (a : ι →₀ R) (_ : ∀ (i : ι), a i I), (a.sum fun (i : ι) (c : R) => c f i) = x

      If x is an I-multiple of the submodule spanned by f '' s, then we can write x as an I-linear combination of the elements of f '' s.

      theorem Submodule.mem_ideal_smul_span_iff_exists_sum' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) {ι : Type u_4} (s : Set ι) (f : ιM) (x : M) :
      x I Submodule.span R (f '' s) ∃ (a : s →₀ R) (_ : ∀ (i : s), a i I), (a.sum fun (i : s) (c : R) => c f i) = x
      theorem Submodule.mem_smul_top_iff {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) (x : N) :
      x I x I N
      @[simp]
      theorem Submodule.smul_comap_le_comap_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R) :
      @[simp]
      theorem Ideal.add_eq_sup {R : Type u} [Semiring R] {I : Ideal R} {J : Ideal R} :
      I + J = I J
      @[simp]
      theorem Ideal.zero_eq_bot {R : Type u} [Semiring R] :
      0 =
      @[simp]
      theorem Ideal.sum_eq_sup {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ιIdeal R) :
      s.sum f = s.sup f
      instance Ideal.instMul {R : Type u} [CommSemiring R] :
      Equations
      • Ideal.instMul = { mul := fun (x x_1 : Ideal R) => x x_1 }
      @[simp]
      theorem Ideal.one_eq_top {R : Type u} [CommSemiring R] :
      1 =
      theorem Ideal.add_eq_one_iff {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      I + J = 1 iI, jJ, i + j = 1
      theorem Ideal.mul_mem_mul {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {r : R} {s : R} (hr : r I) (hs : s J) :
      r * s I * J
      theorem Ideal.mul_mem_mul_rev {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {r : R} {s : R} (hr : r I) (hs : s J) :
      s * r I * J
      theorem Ideal.pow_mem_pow {R : Type u} [CommSemiring R] {I : Ideal R} {x : R} (hx : x I) (n : ) :
      x ^ n I ^ n
      theorem Ideal.prod_mem_prod {R : Type u} [CommSemiring R] {ι : Type u_2} {s : Finset ι} {I : ιIdeal R} {x : ιR} :
      (is, x i I i)is, x i is, I i
      theorem Ideal.mul_le {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} :
      I * J K rI, sJ, r * s K
      theorem Ideal.mul_le_left {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      I * J J
      theorem Ideal.mul_le_right {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      I * J I
      @[simp]
      theorem Ideal.sup_mul_right_self {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      I I * J = I
      @[simp]
      theorem Ideal.sup_mul_left_self {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      I J * I = I
      @[simp]
      theorem Ideal.mul_right_self_sup {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      I * J I = I
      @[simp]
      theorem Ideal.mul_left_self_sup {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      J * I I = I
      theorem Ideal.mul_comm {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) :
      I * J = J * I
      theorem Ideal.mul_assoc {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) (K : Ideal R) :
      I * J * K = I * (J * K)
      theorem Ideal.span_mul_span {R : Type u} [CommSemiring R] (S : Set R) (T : Set R) :
      Ideal.span S * Ideal.span T = Ideal.span (sS, tT, {s * t})
      theorem Ideal.span_mul_span' {R : Type u} [CommSemiring R] (S : Set R) (T : Set R) :
      theorem Ideal.span_singleton_pow {R : Type u} [CommSemiring R] (s : R) (n : ) :
      Ideal.span {s} ^ n = Ideal.span {s ^ n}
      theorem Ideal.mem_mul_span_singleton {R : Type u} [CommSemiring R] {x : R} {y : R} {I : Ideal R} :
      x I * Ideal.span {y} zI, z * y = x
      theorem Ideal.mem_span_singleton_mul {R : Type u} [CommSemiring R] {x : R} {y : R} {I : Ideal R} :
      x Ideal.span {y} * I zI, y * z = x
      theorem Ideal.le_span_singleton_mul_iff {R : Type u} [CommSemiring R] {x : R} {I : Ideal R} {J : Ideal R} :
      I Ideal.span {x} * J zII, zJJ, x * zJ = zI
      theorem Ideal.span_singleton_mul_le_iff {R : Type u} [CommSemiring R] {x : R} {I : Ideal R} {J : Ideal R} :
      Ideal.span {x} * I J zI, x * z J
      theorem Ideal.span_singleton_mul_le_span_singleton_mul {R : Type u} [CommSemiring R] {x : R} {y : R} {I : Ideal R} {J : Ideal R} :
      Ideal.span {x} * I Ideal.span {y} * J zII, zJJ, x * zI = y * zJ
      theorem Ideal.span_singleton_mul_right_mono {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {x : R} (hx : x 0) :
      Ideal.span {x} * I Ideal.span {x} * J I J
      theorem Ideal.span_singleton_mul_left_mono {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {x : R} (hx : x 0) :
      I * Ideal.span {x} J * Ideal.span {x} I J
      theorem Ideal.span_singleton_mul_right_inj {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {x : R} (hx : x 0) :
      Ideal.span {x} * I = Ideal.span {x} * J I = J
      theorem Ideal.span_singleton_mul_left_inj {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {x : R} (hx : x 0) :
      I * Ideal.span {x} = J * Ideal.span {x} I = J
      theorem Ideal.span_singleton_mul_right_injective {R : Type u} [CommSemiring R] [IsDomain R] {x : R} (hx : x 0) :
      Function.Injective fun (x_1 : Ideal R) => Ideal.span {x} * x_1
      theorem Ideal.span_singleton_mul_left_injective {R : Type u} [CommSemiring R] [IsDomain R] {x : R} (hx : x 0) :
      Function.Injective fun (I : Ideal R) => I * Ideal.span {x}
      theorem Ideal.eq_span_singleton_mul {R : Type u} [CommSemiring R] {x : R} (I : Ideal R) (J : Ideal R) :
      I = Ideal.span {x} * J (zII, zJJ, x * zJ = zI) zJ, x * z I
      theorem Ideal.span_singleton_mul_eq_span_singleton_mul {R : Type u} [CommSemiring R] {x : R} {y : R} (I : Ideal R) (J : Ideal R) :
      Ideal.span {x} * I = Ideal.span {y} * J (zII, zJJ, x * zI = y * zJ) zJJ, zII, x * zI = y * zJ
      theorem Ideal.prod_span {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ιSet R) :
      is, Ideal.span (I i) = Ideal.span (is, I i)
      theorem Ideal.prod_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ιR) :
      is, Ideal.span {I i} = Ideal.span {is, I i}
      @[simp]
      theorem Ideal.multiset_prod_span_singleton {R : Type u} [CommSemiring R] (m : Multiset R) :
      (Multiset.map (fun (x : R) => Ideal.span {x}) m).prod = Ideal.span {m.prod}
      theorem Ideal.finset_inf_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ιR) (hI : (s).Pairwise (IsCoprime on I)) :
      (s.inf fun (i : ι) => Ideal.span {I i}) = Ideal.span {is, I i}
      theorem Ideal.iInf_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} [Fintype ι] {I : ιR} (hI : ∀ (i j : ι), i jIsCoprime (I i) (I j)) :
      ⨅ (i : ι), Ideal.span {I i} = Ideal.span {i : ι, I i}
      theorem Ideal.iInf_span_singleton_natCast {R : Type u_2} [CommRing R] {ι : Type u_3} [Fintype ι] {I : ι} (hI : Pairwise fun (i j : ι) => (I i).Coprime (I j)) :
      ⨅ (i : ι), Ideal.span {(I i)} = Ideal.span {(i : ι, I i)}
      theorem Ideal.mul_le_inf {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      I * J I J
      theorem Ideal.multiset_prod_le_inf {R : Type u} [CommSemiring R] {s : Multiset (Ideal R)} :
      s.prod s.inf
      theorem Ideal.prod_le_inf {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ιIdeal R} :
      s.prod f s.inf f
      theorem Ideal.mul_eq_inf_of_coprime {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (h : I J = ) :
      I * J = I J
      theorem Ideal.sup_mul_eq_of_coprime_left {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (h : I J = ) :
      I J * K = I K
      theorem Ideal.sup_mul_eq_of_coprime_right {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (h : I K = ) :
      I J * K = I J
      theorem Ideal.mul_sup_eq_of_coprime_left {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (h : I J = ) :
      I * K J = K J
      theorem Ideal.mul_sup_eq_of_coprime_right {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (h : K J = ) :
      I * K J = I J
      theorem Ideal.sup_prod_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ιIdeal R} (h : is, I J i = ) :
      I is, J i =
      theorem Ideal.sup_iInf_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ιIdeal R} (h : is, I J i = ) :
      I is, J i =
      theorem Ideal.prod_sup_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ιIdeal R} (h : is, J i I = ) :
      (is, J i) I =
      theorem Ideal.iInf_sup_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ιIdeal R} (h : is, J i I = ) :
      (is, J i) I =
      theorem Ideal.sup_pow_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {n : } (h : I J = ) :
      I J ^ n =
      theorem Ideal.pow_sup_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {n : } (h : I J = ) :
      I ^ n J =
      theorem Ideal.pow_sup_pow_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {m : } {n : } (h : I J = ) :
      I ^ m J ^ n =
      theorem Ideal.mul_bot {R : Type u} [CommSemiring R] (I : Ideal R) :
      theorem Ideal.bot_mul {R : Type u} [CommSemiring R] (I : Ideal R) :
      @[simp]
      theorem Ideal.mul_top {R : Type u} [CommSemiring R] (I : Ideal R) :
      I * = I
      @[simp]
      theorem Ideal.top_mul {R : Type u} [CommSemiring R] (I : Ideal R) :
      * I = I
      theorem Ideal.mul_mono {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} {L : Ideal R} (hik : I K) (hjl : J L) :
      I * J K * L
      theorem Ideal.mul_mono_left {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (h : I J) :
      I * K J * K
      theorem Ideal.mul_mono_right {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (h : J K) :
      I * J I * K
      theorem Ideal.mul_sup {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) (K : Ideal R) :
      I * (J K) = I * J I * K
      theorem Ideal.sup_mul {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) (K : Ideal R) :
      (I J) * K = I * K J * K
      theorem Ideal.pow_le_pow_right {R : Type u} [CommSemiring R] {I : Ideal R} {m : } {n : } (h : m n) :
      I ^ n I ^ m
      theorem Ideal.pow_le_self {R : Type u} [CommSemiring R] {I : Ideal R} {n : } (hn : n 0) :
      I ^ n I
      theorem Ideal.pow_right_mono {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (e : I J) (n : ) :
      I ^ n J ^ n
      @[simp]
      theorem Ideal.mul_eq_bot {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] {I : Ideal R} {J : Ideal R} :
      I * J = I = J =
      Equations
      • =
      Equations
      • =
      @[simp]
      theorem Ideal.multiset_prod_eq_bot {R : Type u_2} [CommRing R] [IsDomain R] {s : Multiset (Ideal R)} :
      s.prod = s

      A product of ideals in an integral domain is zero if and only if one of the terms is zero.

      @[deprecated Ideal.multiset_prod_eq_bot]
      theorem Ideal.prod_eq_bot {R : Type u_2} [CommRing R] [IsDomain R] {s : Multiset (Ideal R)} :
      s.prod = Is, I =

      A product of ideals in an integral domain is zero if and only if one of the terms is zero.

      theorem Ideal.span_pair_mul_span_pair {R : Type u} [CommSemiring R] (w : R) (x : R) (y : R) (z : R) :
      Ideal.span {w, x} * Ideal.span {y, z} = Ideal.span {w * y, w * z, x * y, x * z}
      theorem Ideal.isCoprime_iff_add {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      IsCoprime I J I + J = 1
      theorem Ideal.isCoprime_iff_exists {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      IsCoprime I J iI, jJ, i + j = 1
      theorem Ideal.isCoprime_iff_sup_eq {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      theorem Ideal.isCoprime_tfae {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
      [IsCoprime I J, Codisjoint I J, I + J = 1, iI, jJ, i + j = 1, I J = ].TFAE
      theorem IsCoprime.codisjoint {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (h : IsCoprime I J) :
      theorem IsCoprime.add_eq {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (h : IsCoprime I J) :
      I + J = 1
      theorem IsCoprime.exists {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (h : IsCoprime I J) :
      iI, jJ, i + j = 1
      theorem IsCoprime.sup_eq {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (h : IsCoprime I J) :
      I J =
      theorem Ideal.inf_eq_mul_of_isCoprime {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (coprime : IsCoprime I J) :
      I J = I * J
      @[deprecated Ideal.inf_eq_mul_of_isCoprime]
      theorem Ideal.inf_eq_mul_of_coprime {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (coprime : IsCoprime I J) :
      I J = I * J

      Alias of Ideal.inf_eq_mul_of_isCoprime.

      theorem Ideal.isCoprime_biInf {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {J : ιIdeal R} {s : Finset ι} (hf : js, IsCoprime I (J j)) :
      IsCoprime I (js, J j)
      def Ideal.radical {R : Type u} [CommSemiring R] (I : Ideal R) :

      The radical of an ideal I consists of the elements r such that r ^ n ∈ I for some n.

      Equations
      • I.radical = { carrier := {r : R | ∃ (n : ), r ^ n I}, add_mem' := , zero_mem' := , smul_mem' := }
      Instances For
        theorem Ideal.mem_radical_iff {R : Type u} [CommSemiring R] {I : Ideal R} {r : R} :
        r I.radical ∃ (n : ), r ^ n I
        def Ideal.IsRadical {R : Type u} [CommSemiring R] (I : Ideal R) :

        An ideal is radical if it contains its radical.

        Equations
        • I.IsRadical = (I.radical I)
        Instances For
          theorem Ideal.le_radical {R : Type u} [CommSemiring R] {I : Ideal R} :
          I I.radical
          theorem Ideal.radical_eq_iff {R : Type u} [CommSemiring R] {I : Ideal R} :
          I.radical = I I.IsRadical

          An ideal is radical iff it is equal to its radical.

          theorem Ideal.IsRadical.radical {R : Type u} [CommSemiring R] {I : Ideal R} :
          I.IsRadicalI.radical = I

          Alias of the reverse direction of Ideal.radical_eq_iff.


          An ideal is radical iff it is equal to its radical.

          theorem Ideal.isRadical_iff_pow_one_lt {R : Type u} [CommSemiring R] {I : Ideal R} (k : ) (hk : 1 < k) :
          I.IsRadical ∀ (r : R), r ^ k Ir I
          theorem Ideal.radical_top (R : Type u) [CommSemiring R] :
          .radical =
          theorem Ideal.radical_mono {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (H : I J) :
          I.radical J.radical
          theorem Ideal.radical_isRadical {R : Type u} [CommSemiring R] (I : Ideal R) :
          I.radical.IsRadical
          @[simp]
          theorem Ideal.radical_idem {R : Type u} [CommSemiring R] (I : Ideal R) :
          I.radical.radical = I.radical
          theorem Ideal.IsRadical.radical_le_iff {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (hJ : J.IsRadical) :
          I.radical J I J
          theorem Ideal.radical_le_radical_iff {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
          I.radical J.radical I J.radical
          theorem Ideal.radical_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} :
          I.radical = I =
          theorem Ideal.IsPrime.isRadical {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) :
          I.IsRadical
          theorem Ideal.IsPrime.radical {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) :
          I.radical = I
          theorem Ideal.mem_radical_of_pow_mem {R : Type u} [CommSemiring R] {I : Ideal R} {x : R} {m : } (hx : x ^ m I.radical) :
          x I.radical
          theorem Ideal.disjoint_powers_iff_not_mem {R : Type u} [CommSemiring R] {I : Ideal R} (y : R) (hI : I.IsRadical) :
          Disjoint (Submonoid.powers y) I yI.toAddSubmonoid
          theorem Ideal.radical_sup {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) :
          (I J).radical = (I.radical J.radical).radical
          theorem Ideal.radical_inf {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) :
          (I J).radical = I.radical J.radical
          theorem Ideal.IsRadical.inf {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (hI : I.IsRadical) (hJ : J.IsRadical) :
          (I J).IsRadical
          theorem Ideal.radical_iInf_le {R : Type u} [CommSemiring R] {ι : Sort u_2} (I : ιIdeal R) :
          (⨅ (i : ι), I i).radical ⨅ (i : ι), (I i).radical

          The reverse inclusion does not hold for e.g. I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}.

          theorem Ideal.isRadical_iInf {R : Type u} [CommSemiring R] {ι : Sort u_2} (I : ιIdeal R) (hI : ∀ (i : ι), (I i).IsRadical) :
          (⨅ (i : ι), I i).IsRadical
          theorem Ideal.radical_mul {R : Type u} [CommSemiring R] (I : Ideal R) (J : Ideal R) :
          (I * J).radical = I.radical J.radical
          theorem Ideal.IsPrime.radical_le_iff {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} (hJ : J.IsPrime) :
          I.radical J I J
          theorem Ideal.radical_eq_sInf {R : Type u} [CommSemiring R] (I : Ideal R) :
          I.radical = sInf {J : Ideal R | I J J.IsPrime}
          Equations
          • Ideal.instIdemCommSemiring = inferInstance
          theorem Ideal.top_pow (R : Type u) [CommSemiring R] (n : ) :
          theorem Ideal.radical_pow {R : Type u} [CommSemiring R] (I : Ideal R) {n : } :
          n 0(I ^ n).radical = I.radical
          theorem Ideal.IsPrime.mul_le {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {P : Ideal R} (hp : P.IsPrime) :
          I * J P I P J P
          theorem Ideal.IsPrime.inf_le {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {P : Ideal R} (hp : P.IsPrime) :
          I J P I P J P
          theorem Ideal.IsPrime.multiset_prod_le {R : Type u} [CommSemiring R] {s : Multiset (Ideal R)} {P : Ideal R} (hp : P.IsPrime) :
          s.prod P Is, I P
          theorem Ideal.IsPrime.multiset_prod_map_le {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Multiset ι} (f : ιIdeal R) {P : Ideal R} (hp : P.IsPrime) :
          (Multiset.map f s).prod P is, f i P
          theorem Ideal.IsPrime.multiset_prod_mem_iff_exists_mem {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Multiset R) :
          s.prod I ps, p I
          theorem Ideal.IsPrime.prod_le {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ιIdeal R} {P : Ideal R} (hp : P.IsPrime) :
          s.prod f P is, f i P
          theorem Ideal.IsPrime.prod_mem_iff_exists_mem {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Finset R) :
          xs, x I ps, p I
          theorem Ideal.IsPrime.inf_le' {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ιIdeal R} {P : Ideal R} (hp : P.IsPrime) :
          s.inf f P is, f i P
          theorem Ideal.subset_union {R : Type u} [Ring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} :
          I J K I J I K
          theorem Ideal.subset_union_prime' {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ιIdeal R} {a : ι} {b : ι} (hp : is, (f i).IsPrime) {I : Ideal R} :
          I (f a) (f b) is, (f i) I f a I f b is, I f i
          theorem Ideal.subset_union_prime {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ιIdeal R} (a : ι) (b : ι) (hp : is, i ai b(f i).IsPrime) {I : Ideal R} :
          I is, (f i) is, I f i

          Prime avoidance. Atiyah-Macdonald 1.11, Eisenbud 3.3, Stacks 00DS, Matsumura Ex.1.6.

          theorem Ideal.le_of_dvd {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} :
          I JJ I

          If I divides J, then I contains J.

          In a Dedekind domain, to divide and contain are equivalent, see Ideal.dvd_iff_le.

          @[simp]
          theorem Ideal.isUnit_iff {R : Type u} [CommSemiring R] {I : Ideal R} :
          Equations
          • Ideal.uniqueUnits = { default := 1, uniq := }
          noncomputable def Ideal.finsuppTotal (ι : Type u_1) (M : Type u_2) [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) (v : ιM) :
          (ι →₀ I) →ₗ[R] M

          A variant of Finsupp.total that takes in vectors valued in I.

          Equations
          Instances For
            theorem Ideal.finsuppTotal_apply {ι : Type u_1} {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) {v : ιM} (f : ι →₀ I) :
            (Ideal.finsuppTotal ι M I v) f = f.sum fun (i : ι) (x : I) => x v i
            theorem Ideal.finsuppTotal_apply_eq_of_fintype {ι : Type u_1} {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) {v : ιM} [Fintype ι] (f : ι →₀ I) :
            (Ideal.finsuppTotal ι M I v) f = i : ι, (f i) v i
            theorem Ideal.range_finsuppTotal {ι : Type u_1} {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) {v : ιM} :
            theorem Finsupp.mem_ideal_span_range_iff_exists_finsupp {α : Type u_1} {R : Type u_2} [Semiring R] {x : R} {v : αR} :
            x Ideal.span (Set.range v) ∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) => a * v i) = x
            theorem mem_ideal_span_range_iff_exists_fun {α : Type u_1} {R : Type u_2} [Semiring R] [Fintype α] {x : R} {v : αR} :
            x Ideal.span (Set.range v) ∃ (c : αR), i : α, c i * v i = x

            An element x lies in the span of v iff it can be written as sum ∑ cᵢ • vᵢ = x.

            instance Submodule.moduleSubmodule {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
            Equations
            theorem Submodule.span_smul_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (N : Submodule R M) :
            @[simp]