More operations on modules and ideals #

instance Submodule.hasSMul' {R : Type u} {M : Type v} [] [] [Module R M] :
SMul () ()
Equations
• Submodule.hasSMul' = { smul := }
theorem Ideal.smul_eq_mul {R : Type u} [] (I : ) (J : ) :
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) [] [] [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} [] [] [Module R M] {r : R} :
r ∀ (m : M), r m = 0
theorem LinearMap.annihilator_le_of_injective {R : Type u} {M : Type v} {M' : Type u_1} [] [] [Module R M] [] [Module R M'] (f : M →ₗ[R] M') (hf : ) :
theorem LinearMap.annihilator_le_of_surjective {R : Type u} {M : Type v} {M' : Type u_1} [] [] [Module R M] [] [Module R M'] (f : M →ₗ[R] M') (hf : ) :
theorem LinearEquiv.annihilator_eq {R : Type u} {M : Type v} {M' : Type u_1} [] [] [Module R M] [] [Module R M'] (e : M ≃ₗ[R] M') :
@[reducible, inline]
abbrev Submodule.annihilator {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :

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

Equations
• N.annihilator =
Instances For
theorem Submodule.annihilator_top {R : Type u} {M : Type v} [] [] [Module R M] :
.annihilator =
theorem Submodule.mem_annihilator {R : Type u} {M : Type v} [] [] [Module R M] {N : } {r : R} :
r N.annihilator nN, r n = 0
theorem Submodule.mem_annihilator' {R : Type u} {M : Type v} [] [] [Module R M] {N : } {r : R} :
r N.annihilator N Submodule.comap (r LinearMap.id)
theorem Submodule.mem_annihilator_span {R : Type u} {M : Type v} [] [] [Module R M] (s : Set M) (r : R) :
r ().annihilator ∀ (n : s), r n = 0
theorem Submodule.mem_annihilator_span_singleton {R : Type u} {M : Type v} [] [] [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} [] [] [Module R M] :
.annihilator =
theorem Submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [] [] [Module R M] {N : } :
N.annihilator = N =
theorem Submodule.annihilator_mono {R : Type u} {M : Type v} [] [] [Module R M] {N : } {P : } (h : N P) :
P.annihilator N.annihilator
theorem Submodule.annihilator_iSup {R : Type u} {M : Type v} [] [] [Module R M] (ι : Sort w) (f : ι) :
(⨆ (i : ι), f i).annihilator = ⨅ (i : ι), (f i).annihilator
theorem Submodule.smul_mem_smul {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {r : R} {n : M} (hr : r I) (hn : n N) :
r n I N
theorem Submodule.smul_le {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {P : } :
I N P rI, nN, r n P
@[simp]
theorem Submodule.coe_set_smul {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } :
I N = I N
theorem Submodule.smul_induction_on {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {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} [] [] [Module R M] {I : } {N : } {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} [] [] [Module R M] {I : } {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} [] [] [Module R M] {I : } {N : } :
I N N
theorem Submodule.smul_mono {R : Type u} {M : Type v} [] [] [Module R M] {I : } {J : } {N : } {P : } (hij : I J) (hnp : N P) :
I N J P
theorem Submodule.smul_mono_left {R : Type u} {M : Type v} [] [] [Module R M] {I : } {J : } {N : } (h : I J) :
I N J N
instance Submodule.instCovariantClassIdealHSMulLe {R : Type u} {M : Type v} [] [] [Module R M] :
CovariantClass () () HSMul.hSMul LE.le
Equations
• =
@[deprecated smul_mono_right]
theorem Submodule.smul_mono_right {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {P : } (h : N P) :
I N I P
theorem Submodule.map_le_smul_top {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (f : R →ₗ[R] M) :
@[simp]
theorem Submodule.annihilator_smul {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :
N.annihilator N =
@[simp]
theorem Submodule.annihilator_mul {R : Type u} [] (I : ) :
@[simp]
theorem Submodule.mul_annihilator {R : Type u} [] (I : ) :
@[simp]
theorem Submodule.smul_bot {R : Type u} {M : Type v} [] [] [Module R M] (I : ) :
@[simp]
theorem Submodule.bot_smul {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :
@[simp]
theorem Submodule.top_smul {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :
N = N
theorem Submodule.smul_sup {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (N : ) (P : ) :
I (N P) = I N I P
theorem Submodule.sup_smul {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (J : ) (N : ) :
(I J) N = I N J N
theorem Submodule.smul_assoc {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (J : ) (N : ) :
(I J) N = I J N
@[deprecated smul_inf_le]
theorem Submodule.smul_inf_le {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (M₁ : ) (M₂ : ) :
I (M₁ M₂) I M₁ I M₂
theorem Submodule.smul_iSup {R : Type u} {M : Type v} [] [] [Module R M] {ι : Sort u_4} {I : } {t : ι} :
I iSup t = ⨆ (i : ι), I t i
@[deprecated smul_iInf_le]
theorem Submodule.smul_iInf_le {R : Type u} {M : Type v} [] [] [Module R M] {ι : Sort u_4} {I : } {t : ι} :
I iInf t ⨅ (i : ι), I t i
theorem Submodule.span_smul_span {R : Type u} {M : Type v} [] [] [Module R M] (S : Set R) (T : Set M) :
= Submodule.span R (sS, tT, {s t})
theorem Submodule.ideal_span_singleton_smul {R : Type u} {M : Type v} [] [] [Module R M] (r : R) (N : ) :
Ideal.span {r} N = r N
theorem Submodule.mem_of_span_top_of_smul_mem {R : Type u} {M : Type v} [] [] [Module R M] (M' : ) (s : Set R) (hs : ) (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} [] [] [Module R M] (M' : ) (s : Set R) (hs : ) (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.

theorem Submodule.map_smul'' {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (N : ) {M' : Type w} [] [Module R M'] (f : M →ₗ[R] M') :
Submodule.map f (I N) = I
theorem Submodule.mem_smul_span {R : Type u} {M : Type v} [] [] [Module R M] {I : } {s : Set M} {x : M} :
x I x Submodule.span R (aI, bs, {a b})
theorem Submodule.mem_ideal_smul_span_iff_exists_sum {R : Type u} {M : Type v} [] [] [Module R M] (I : ) {ι : Type u_4} (f : ιM) (x : M) :
x I ∃ (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} [] [] [Module R M] (I : ) {ι : 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} [] [] [Module R M] (I : ) (N : ) (x : N) :
x I x I N
@[simp]
theorem Submodule.smul_comap_le_comap_smul {R : Type u} {M : Type v} [] [] [Module R M] {M' : Type w} [] [Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (I : ) :
@[simp]
theorem Ideal.add_eq_sup {R : Type u} [] {I : } {J : } :
I + J = I J
@[simp]
theorem Ideal.zero_eq_bot {R : Type u} [] :
0 =
@[simp]
theorem Ideal.sum_eq_sup {R : Type u} [] {ι : Type u_1} (s : ) (f : ι) :
s.sum f = s.sup f
instance Ideal.instMul {R : Type u} [] :
Mul ()
Equations
• Ideal.instMul = { mul := fun (x x_1 : ) => x x_1 }
@[simp]
theorem Ideal.one_eq_top {R : Type u} [] :
1 =
theorem Ideal.add_eq_one_iff {R : Type u} [] {I : } {J : } :
I + J = 1 iI, jJ, i + j = 1
theorem Ideal.mul_mem_mul {R : Type u} [] {I : } {J : } {r : R} {s : R} (hr : r I) (hs : s J) :
r * s I * J
theorem Ideal.mul_mem_mul_rev {R : Type u} [] {I : } {J : } {r : R} {s : R} (hr : r I) (hs : s J) :
s * r I * J
theorem Ideal.pow_mem_pow {R : Type u} [] {I : } {x : R} (hx : x I) (n : ) :
x ^ n I ^ n
theorem Ideal.prod_mem_prod {R : Type u} [] {ι : Type u_2} {s : } {I : ι} {x : ιR} :
(is, x i I i)(s.prod fun (i : ι) => x i) s.prod fun (i : ι) => I i
theorem Ideal.mul_le {R : Type u} [] {I : } {J : } {K : } :
I * J K rI, sJ, r * s K
theorem Ideal.mul_le_left {R : Type u} [] {I : } {J : } :
I * J J
theorem Ideal.mul_le_right {R : Type u} [] {I : } {J : } :
I * J I
@[simp]
theorem Ideal.sup_mul_right_self {R : Type u} [] {I : } {J : } :
I I * J = I
@[simp]
theorem Ideal.sup_mul_left_self {R : Type u} [] {I : } {J : } :
I J * I = I
@[simp]
theorem Ideal.mul_right_self_sup {R : Type u} [] {I : } {J : } :
I * J I = I
@[simp]
theorem Ideal.mul_left_self_sup {R : Type u} [] {I : } {J : } :
J * I I = I
theorem Ideal.mul_comm {R : Type u} [] (I : ) (J : ) :
I * J = J * I
theorem Ideal.mul_assoc {R : Type u} [] (I : ) (J : ) (K : ) :
I * J * K = I * (J * K)
theorem Ideal.span_mul_span {R : Type u} [] (S : Set R) (T : Set R) :
= Ideal.span (sS, tT, {s * t})
theorem Ideal.span_mul_span' {R : Type u} [] (S : Set R) (T : Set R) :
= Ideal.span (S * T)
theorem Ideal.span_singleton_mul_span_singleton {R : Type u} [] (r : R) (s : R) :
theorem Ideal.span_singleton_pow {R : Type u} [] (s : R) (n : ) :
Ideal.span {s} ^ n = Ideal.span {s ^ n}
theorem Ideal.mem_mul_span_singleton {R : Type u} [] {x : R} {y : R} {I : } :
x I * Ideal.span {y} zI, z * y = x
theorem Ideal.mem_span_singleton_mul {R : Type u} [] {x : R} {y : R} {I : } :
x Ideal.span {y} * I zI, y * z = x
theorem Ideal.le_span_singleton_mul_iff {R : Type u} [] {x : R} {I : } {J : } :
I Ideal.span {x} * J zII, zJJ, x * zJ = zI
theorem Ideal.span_singleton_mul_le_iff {R : Type u} [] {x : R} {I : } {J : } :
Ideal.span {x} * I J zI, x * z J
theorem Ideal.span_singleton_mul_le_span_singleton_mul {R : Type u} [] {x : R} {y : R} {I : } {J : } :
Ideal.span {x} * I Ideal.span {y} * J zII, zJJ, x * zI = y * zJ
theorem Ideal.span_singleton_mul_right_mono {R : Type u} [] {I : } {J : } [] {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} [] {I : } {J : } [] {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} [] {I : } {J : } [] {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} [] {I : } {J : } [] {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} [] [] {x : R} (hx : x 0) :
Function.Injective fun (x_1 : ) => Ideal.span {x} * x_1
theorem Ideal.span_singleton_mul_left_injective {R : Type u} [] [] {x : R} (hx : x 0) :
Function.Injective fun (I : ) => I * Ideal.span {x}
theorem Ideal.eq_span_singleton_mul {R : Type u} [] {x : R} (I : ) (J : ) :
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} [] {x : R} {y : R} (I : ) (J : ) :
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} [] {ι : Type u_2} (s : ) (I : ιSet R) :
(s.prod fun (i : ι) => Ideal.span (I i)) = Ideal.span (s.prod fun (i : ι) => I i)
theorem Ideal.prod_span_singleton {R : Type u} [] {ι : Type u_2} (s : ) (I : ιR) :
(s.prod fun (i : ι) => Ideal.span {I i}) = Ideal.span {s.prod fun (i : ι) => I i}
@[simp]
theorem Ideal.multiset_prod_span_singleton {R : Type u} [] (m : ) :
(Multiset.map (fun (x : R) => Ideal.span {x}) m).prod = Ideal.span {m.prod}
theorem Ideal.finset_inf_span_singleton {R : Type u} [] {ι : Type u_2} (s : ) (I : ιR) (hI : (s).Pairwise (IsCoprime on I)) :
(s.inf fun (i : ι) => Ideal.span {I i}) = Ideal.span {s.prod fun (i : ι) => I i}
theorem Ideal.iInf_span_singleton {R : Type u} [] {ι : Type u_2} [] {I : ιR} (hI : ∀ (i j : ι), i jIsCoprime (I i) (I j)) :
⨅ (i : ι), Ideal.span {I i} = Ideal.span {Finset.univ.prod fun (i : ι) => I i}
theorem Ideal.iInf_span_singleton_natCast {R : Type u_2} [] {ι : Type u_3} [] {I : ι} (hI : Pairwise fun (i j : ι) => (I i).Coprime (I j)) :
⨅ (i : ι), Ideal.span {(I i)} = Ideal.span {(Finset.univ.prod fun (i : ι) => I i)}
theorem Ideal.sup_eq_top_iff_isCoprime {R : Type u_2} [] (x : R) (y : R) :
theorem Ideal.mul_le_inf {R : Type u} [] {I : } {J : } :
I * J I J
theorem Ideal.multiset_prod_le_inf {R : Type u} [] {s : Multiset ()} :
s.prod s.inf
theorem Ideal.prod_le_inf {R : Type u} {ι : Type u_1} [] {s : } {f : ι} :
s.prod f s.inf f
theorem Ideal.mul_eq_inf_of_coprime {R : Type u} [] {I : } {J : } (h : I J = ) :
I * J = I J
theorem Ideal.sup_mul_eq_of_coprime_left {R : Type u} [] {I : } {J : } {K : } (h : I J = ) :
I J * K = I K
theorem Ideal.sup_mul_eq_of_coprime_right {R : Type u} [] {I : } {J : } {K : } (h : I K = ) :
I J * K = I J
theorem Ideal.mul_sup_eq_of_coprime_left {R : Type u} [] {I : } {J : } {K : } (h : I J = ) :
I * K J = K J
theorem Ideal.mul_sup_eq_of_coprime_right {R : Type u} [] {I : } {J : } {K : } (h : K J = ) :
I * K J = I J
theorem Ideal.sup_prod_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : is, I J i = ) :
(I s.prod fun (i : ι) => J i) =
theorem Ideal.sup_iInf_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : is, I J i = ) :
I is, J i =
theorem Ideal.prod_sup_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : is, J i I = ) :
(s.prod fun (i : ι) => J i) I =
theorem Ideal.iInf_sup_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : is, J i I = ) :
(is, J i) I =
theorem Ideal.sup_pow_eq_top {R : Type u} [] {I : } {J : } {n : } (h : I J = ) :
I J ^ n =
theorem Ideal.pow_sup_eq_top {R : Type u} [] {I : } {J : } {n : } (h : I J = ) :
I ^ n J =
theorem Ideal.pow_sup_pow_eq_top {R : Type u} [] {I : } {J : } {m : } {n : } (h : I J = ) :
I ^ m J ^ n =
theorem Ideal.mul_bot {R : Type u} [] (I : ) :
theorem Ideal.bot_mul {R : Type u} [] (I : ) :
@[simp]
theorem Ideal.mul_top {R : Type u} [] (I : ) :
I * = I
@[simp]
theorem Ideal.top_mul {R : Type u} [] (I : ) :
* I = I
theorem Ideal.mul_mono {R : Type u} [] {I : } {J : } {K : } {L : } (hik : I K) (hjl : J L) :
I * J K * L
theorem Ideal.mul_mono_left {R : Type u} [] {I : } {J : } {K : } (h : I J) :
I * K J * K
theorem Ideal.mul_mono_right {R : Type u} [] {I : } {J : } {K : } (h : J K) :
I * J I * K
theorem Ideal.mul_sup {R : Type u} [] (I : ) (J : ) (K : ) :
I * (J K) = I * J I * K
theorem Ideal.sup_mul {R : Type u} [] (I : ) (J : ) (K : ) :
(I J) * K = I * K J * K
theorem Ideal.pow_le_pow_right {R : Type u} [] {I : } {m : } {n : } (h : m n) :
I ^ n I ^ m
theorem Ideal.pow_le_self {R : Type u} [] {I : } {n : } (hn : n 0) :
I ^ n I
theorem Ideal.pow_right_mono {R : Type u} [] {I : } {J : } (e : I J) (n : ) :
I ^ n J ^ n
@[simp]
theorem Ideal.mul_eq_bot {R : Type u_2} [] [] {I : } {J : } :
I * J = I = J =
instance Ideal.instNoZeroDivisors {R : Type u_2} [] [] :
Equations
• =
instance Ideal.instNoZeroSMulDivisorsSubtypeMem {R : Type u_2} [] {S : Type u_3} [] [Algebra R S] [] {I : } :
Equations
• =
@[simp]
theorem Ideal.multiset_prod_eq_bot {R : Type u_2} [] [] {s : Multiset ()} :
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} [] [] {s : Multiset ()} :
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} [] (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_codisjoint {R : Type u} [] {I : } {J : } :
theorem Ideal.isCoprime_iff_add {R : Type u} [] {I : } {J : } :
I + J = 1
theorem Ideal.isCoprime_iff_exists {R : Type u} [] {I : } {J : } :
iI, jJ, i + j = 1
theorem Ideal.isCoprime_iff_sup_eq {R : Type u} [] {I : } {J : } :
I J =
theorem Ideal.isCoprime_tfae {R : Type u} [] {I : } {J : } :
[, , I + J = 1, iI, jJ, i + j = 1, I J = ].TFAE
theorem IsCoprime.codisjoint {R : Type u} [] {I : } {J : } (h : ) :
theorem IsCoprime.add_eq {R : Type u} [] {I : } {J : } (h : ) :
I + J = 1
theorem IsCoprime.exists {R : Type u} [] {I : } {J : } (h : ) :
iI, jJ, i + j = 1
theorem IsCoprime.sup_eq {R : Type u} [] {I : } {J : } (h : ) :
I J =
theorem Ideal.isCoprime_span_singleton_iff {R : Type u} [] (x : R) (y : R) :
theorem Ideal.isCoprime_biInf {R : Type u} {ι : Type u_1} [] {I : } {J : ι} {s : } (hf : js, IsCoprime I (J j)) :
IsCoprime I (js, J j)
def Ideal.radical {R : Type u} [] (I : ) :

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} [] {I : } {r : R} :
r I.radical ∃ (n : ), r ^ n I
def Ideal.IsRadical {R : Type u} [] (I : ) :

Equations
Instances For
theorem Ideal.le_radical {R : Type u} [] {I : } :
theorem Ideal.radical_eq_iff {R : Type u} [] {I : } :

Alias of the reverse direction of Ideal.radical_eq_iff.

theorem Ideal.isRadical_iff_pow_one_lt {R : Type u} [] {I : } (k : ) (hk : 1 < k) :
I.IsRadical ∀ (r : R), r ^ k Ir I
theorem Ideal.radical_top (R : Type u) [] :
theorem Ideal.radical_mono {R : Type u} [] {I : } {J : } (H : I J) :
@[simp]
theorem Ideal.radical_idem {R : Type u} [] (I : ) :
theorem Ideal.IsRadical.radical_le_iff {R : Type u} [] {I : } {J : } (hJ : J.IsRadical) :
theorem Ideal.radical_le_radical_iff {R : Type u} [] {I : } {J : } :
theorem Ideal.radical_eq_top {R : Type u} [] {I : } :
theorem Ideal.IsPrime.isRadical {R : Type u} [] {I : } (H : I.IsPrime) :
theorem Ideal.IsPrime.radical {R : Type u} [] {I : } (H : I.IsPrime) :
theorem Ideal.mem_radical_of_pow_mem {R : Type u} [] {I : } {x : R} {m : } (hx : x ^ m I.radical) :
theorem Ideal.disjoint_powers_iff_not_mem {R : Type u} [] {I : } (y : R) (hI : I.IsRadical) :
theorem Ideal.radical_sup {R : Type u} [] (I : ) (J : ) :
theorem Ideal.radical_inf {R : Type u} [] (I : ) (J : ) :
theorem Ideal.IsRadical.inf {R : Type u} [] {I : } {J : } (hI : I.IsRadical) (hJ : J.IsRadical) :
theorem Ideal.radical_iInf_le {R : Type u} [] {ι : Sort u_2} (I : ι) :
(⨅ (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} [] {ι : Sort u_2} (I : ι) (hI : ∀ (i : ι), (I i).IsRadical) :
(⨅ (i : ι), I i).IsRadical
theorem Ideal.radical_mul {R : Type u} [] (I : ) (J : ) :
theorem Ideal.IsPrime.radical_le_iff {R : Type u} [] {I : } {J : } (hJ : J.IsPrime) :
theorem Ideal.radical_eq_sInf {R : Type u} [] (I : ) :
I.radical = sInf {J : | I J J.IsPrime}
theorem Ideal.isRadical_bot_of_noZeroDivisors {R : Type u_2} [] [] :
@[simp]
theorem Ideal.radical_bot_of_noZeroDivisors {R : Type u} [] [] :
instance Ideal.instIdemCommSemiring {R : Type u} [] :
Equations
• Ideal.instIdemCommSemiring = inferInstance
theorem Ideal.top_pow (R : Type u) [] (n : ) :
theorem Ideal.radical_pow {R : Type u} [] (I : ) {n : } :
theorem Ideal.IsPrime.mul_le {R : Type u} [] {I : } {J : } {P : } (hp : P.IsPrime) :
I * J P I P J P
theorem Ideal.IsPrime.inf_le {R : Type u} [] {I : } {J : } {P : } (hp : P.IsPrime) :
I J P I P J P
theorem Ideal.IsPrime.multiset_prod_le {R : Type u} [] {s : Multiset ()} {P : } (hp : P.IsPrime) :
s.prod P Is, I P
theorem Ideal.IsPrime.multiset_prod_map_le {R : Type u} {ι : Type u_1} [] {s : } (f : ι) {P : } (hp : P.IsPrime) :
().prod P is, f i P
theorem Ideal.IsPrime.multiset_prod_mem_iff_exists_mem {R : Type u} [] {I : } (hI : I.IsPrime) (s : ) :
s.prod I ps, p I
theorem Ideal.IsPrime.prod_le {R : Type u} {ι : Type u_1} [] {s : } {f : ι} {P : } (hp : P.IsPrime) :
s.prod f P is, f i P
theorem Ideal.IsPrime.prod_mem_iff_exists_mem {R : Type u} [] {I : } (hI : I.IsPrime) (s : ) :
(s.prod fun (x : R) => x) I ps, p I
theorem Ideal.IsPrime.inf_le' {R : Type u} {ι : Type u_1} [] {s : } {f : ι} {P : } (hp : P.IsPrime) :
s.inf f P is, f i P
theorem Ideal.subset_union {R : Type u} [Ring R] {I : } {J : } {K : } :
I J K I J I K
theorem Ideal.subset_union_prime' {ι : Type u_1} {R : Type u} [] {s : } {f : ι} {a : ι} {b : ι} (hp : is, (f i).IsPrime) {I : } :
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} [] {s : } {f : ι} (a : ι) (b : ι) (hp : is, i ai b(f i).IsPrime) {I : } :
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} [] {I : } {J : } :
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} [] {I : } :
I =
instance Ideal.uniqueUnits {R : Type u} [] :
Equations
• Ideal.uniqueUnits = { default := 1, uniq := }
noncomputable def Ideal.finsuppTotal (ι : Type u_1) (M : Type u_2) [] {R : Type u_3} [] [Module R M] (I : ) (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} [] {R : Type u_3} [] [Module R M] (I : ) {v : ιM} (f : ι →₀ I) :
() f = f.sum fun (i : ι) (x : I) => x v i
theorem Ideal.finsuppTotal_apply_eq_of_fintype {ι : Type u_1} {M : Type u_2} [] {R : Type u_3} [] [Module R M] (I : ) {v : ιM} [] (f : ι →₀ I) :
() f = Finset.univ.sum fun (i : ι) => (f i) v i
theorem Ideal.range_finsuppTotal {ι : Type u_1} {M : Type u_2} [] {R : Type u_3} [] [Module R M] (I : ) {v : ιM} :
theorem Finsupp.mem_ideal_span_range_iff_exists_finsupp {α : Type u_1} {R : Type u_2} [] {x : R} {v : αR} :
x ∃ (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} [] [] {x : R} {v : αR} :
x ∃ (c : αR), (Finset.univ.sum fun (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.

theorem Associates.mk_ne_zero' {R : Type u_1} [] {r : R} :
instance Submodule.moduleSubmodule {R : Type u} {M : Type v} [] [] [Module R M] :
Module () ()
Equations
• Submodule.moduleSubmodule =
theorem Submodule.span_smul_eq {R : Type u} {M : Type v} [] [] [Module R M] (s : Set R) (N : ) :
N = s N