# More operations on modules and ideals #

source
theorem Submodule.coe_span_smul {R' : Type u_1} {M' : Type u_2} [CommSemiring R'] [AddCommMonoid M'] [Module R' M'] (s : Set R') (N : Submodule R' M') :
↑(Ideal.span s) • N = s • N
source
theorem Submodule.span_singleton_toAddSubgroup_eq_zmultiples (a : ℤ) :
(span ℤ {a}).toAddSubgroup = AddSubgroup.zmultiples a
source
@[simp]
theorem Ideal.span_singleton_toAddSubgroup_eq_zmultiples (a : ℤ) :
Submodule.toAddSubgroup (span {a}) = AddSubgroup.zmultiples a
source
theorem Ideal.smul_eq_mul {R : Type u} [Semiring R] (I 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.

source
theorem Submodule.smul_le_right {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} :
I • N ≤ N
source
theorem Submodule.map_le_smul_top {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (f : R →ₗ[R] M) :
map f I ≤ I • ⊤
source
@[simp]
theorem Submodule.top_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) :
⊤ • N = N
source
theorem Submodule.mul_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I J : Ideal R) (N : Submodule R M) :
(I * J) • N = I • J • N
source
theorem Submodule.mem_of_span_top_of_smul_mem {R : Type u} {M : Type v} [Semiring 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'
source
@[simp]
theorem Submodule.map_smul'' {R : Type u} {M : Type v} [Semiring 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') :
map f (I • N) = I • map f N
source
theorem Submodule.mem_smul_top_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) (x : ↥N) :
x ∈ I • ⊤ ↔ ↑x ∈ I • N
source
@[simp]
theorem Submodule.smul_comap_le_comap_smul {R : Type u} {M : Type v} [Semiring 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) :
I • comap f S ≤ comap f (I • S)
source
theorem Submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} [I.IsTwoSided] {m x : M} :
x ∈ I • span R {m} ↔ ∃ y ∈ I, y • m = x
source
theorem Submodule.span_smul_span {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Set R) (T : Set M) [(Ideal.span S).IsTwoSided] :
Ideal.span S • span R T = span R (S • T)
source
theorem Submodule.mem_smul_span {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} [I.IsTwoSided] {s : Set M} {x : M} :
x ∈ I • span R s ↔ x ∈ span R (↑I • s)
source
theorem Submodule.mem_ideal_smul_span_iff_exists_sum {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) [I.IsTwoSided] {ι : Type u_4} (f : ι → M) (x : M) :
x ∈ I • 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`.

source
theorem Submodule.mem_ideal_smul_span_iff_exists_sum' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) [I.IsTwoSided] {ι : Type u_4} (s : Set ι) (f : ι → M) (x : M) :
x ∈ I • span R (f '' s) ↔ ∃ (a : ↑s →₀ R) (_ : ∀ (i : ↑s), a i ∈ I), (a.sum fun (i : ↑s) (c : R) => c • f ↑i) = x
source
theorem Submodule.smul_eq_map₂ {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} :
I • N = map₂ (LinearMap.lsmul R M) I N
source
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
source
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`.

source
@[simp]
theorem Submodule.map_pointwise_smul {R : Type u} {M : Type v} {M' : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (r : R) (N : Submodule R M) (f : M →ₗ[R] M') :
map f (r • N) = r • map f N
source
@[simp]
theorem Ideal.add_eq_sup {R : Type u} [Semiring R] {I J : Ideal R} :
I + J = I ⊔ J
source
@[simp]
theorem Ideal.zero_eq_bot {R : Type u} [Semiring R] :
0 = ⊥
source
@[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
source
@[simp]
theorem Ideal.one_eq_top {R : Type u} [Semiring R] :
1 = ⊤
source
theorem Ideal.add_eq_one_iff {R : Type u} [Semiring R] {I J : Ideal R} :
I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
source
theorem Ideal.mul_mem_mul {R : Type u} [Semiring R] {I J : Ideal R} {r s : R} (hr : r ∈ I) (hs : s ∈ J) :
r * s ∈ I * J
source
theorem Ideal.bot_pow {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) :
⊥ ^ n = ⊥
source
theorem Ideal.pow_mem_pow {R : Type u} [Semiring R] {I : Ideal R} {x : R} (hx : x ∈ I) (n : ℕ) :
x ^ n ∈ I ^ n
source
theorem Ideal.mul_le {R : Type u} [Semiring R] {I J K : Ideal R} :
I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K
source
theorem Ideal.mul_le_left {R : Type u} [Semiring R] {I J : Ideal R} :
I * J ≤ J
source
@[simp]
theorem Ideal.sup_mul_left_self {R : Type u} [Semiring R] {I J : Ideal R} :
I ⊔ J * I = I
source
@[simp]
theorem Ideal.mul_left_self_sup {R : Type u} [Semiring R] {I J : Ideal R} :
J * I ⊔ I = I
source
theorem Ideal.mul_le_right {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] :
I * J ≤ I
source
@[simp]
theorem Ideal.sup_mul_right_self {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] :
I ⊔ I * J = I
source
@[simp]
theorem Ideal.mul_right_self_sup {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] :
I * J ⊔ I = I
source
theorem Ideal.mul_assoc {R : Type u} [Semiring R] {I J K : Ideal R} :
I * J * K = I * (J * K)
source
theorem Ideal.mul_bot {R : Type u} [Semiring R] (I : Ideal R) :
I * ⊥ = ⊥
source
theorem Ideal.bot_mul {R : Type u} [Semiring R] (I : Ideal R) :
⊥ * I = ⊥
source
@[simp]
theorem Ideal.top_mul {R : Type u} [Semiring R] (I : Ideal R) :
⊤ * I = I
source
theorem Ideal.mul_mono {R : Type u} [Semiring R] {I J K L : Ideal R} (hik : I ≤ K) (hjl : J ≤ L) :
I * J ≤ K * L
source
theorem Ideal.mul_mono_left {R : Type u} [Semiring R] {I J K : Ideal R} (h : I ≤ J) :
I * K ≤ J * K
source
theorem Ideal.mul_mono_right {R : Type u} [Semiring R] {I J K : Ideal R} (h : J ≤ K) :
I * J ≤ I * K
source
theorem Ideal.mul_sup {R : Type u} [Semiring R] (I J K : Ideal R) :
I * (J ⊔ K) = I * J ⊔ I * K
source
theorem Ideal.sup_mul {R : Type u} [Semiring R] (I J K : Ideal R) :
(I ⊔ J) * K = I * K ⊔ J * K
source
theorem Ideal.mul_iSup {R : Type u} [Semiring R] (I : Ideal R) {ι : Sort u_1} (J : ι → Ideal R) :
I * ⨆ (i : ι), J i = ⨆ (i : ι), I * J i
source
theorem Ideal.iSup_mul {R : Type u} [Semiring R] {ι : Sort u_1} (J : ι → Ideal R) (I : Ideal R) :
(⨆ (i : ι), J i) * I = ⨆ (i : ι), J i * I
source
theorem Ideal.pow_le_pow_right {R : Type u} [Semiring R] {I : Ideal R} {m n : ℕ} (h : m ≤ n) :
I ^ n ≤ I ^ m
source
theorem Ideal.pow_le_self {R : Type u} [Semiring R] {I : Ideal R} {n : ℕ} (hn : n ≠ 0) :
I ^ n ≤ I
source
theorem Ideal.pow_right_mono {R : Type u} [Semiring R] {I J : Ideal R} (e : I ≤ J) (n : ℕ) :
I ^ n ≤ J ^ n
source
@[instance 100]
instance Ideal.IsTwoSided.instHMul {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] :
(I * J).IsTwoSided
source
@[instance 100]
instance Ideal.IsTwoSided.instHPowNat {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ) :
(I ^ n).IsTwoSided
source
theorem Ideal.IsTwoSided.mul_one {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] :
I * 1 = I
source
theorem Ideal.IsTwoSided.pow_add {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (m n : ℕ) :
I ^ (m + n) = I ^ m * I ^ n
source
theorem Ideal.IsTwoSided.pow_succ {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ) :
I ^ (n + 1) = I * I ^ n
source
@[simp]
theorem Ideal.mul_eq_bot {R : Type u} [Semiring R] {I J : Ideal R} [NoZeroDivisors R] :
I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥
source
instance Ideal.instNoZeroDivisors {R : Type u} [Semiring R] [NoZeroDivisors R] :
NoZeroDivisors (Ideal R)
source
instance Ideal.instNoZeroSMulDivisorsSubtypeMemSubmodule {R : Type u} [Semiring R] {S : Type u_1} {A : Type u_2} [Semiring S] [SMul R S] [AddCommMonoid A] [Module R A] [Module S A] [IsScalarTower R S A] [NoZeroSMulDivisors R A] {I : Submodule S A} :
NoZeroSMulDivisors R ↥I
source
theorem Ideal.span_mul_span {R : Type u} [Semiring R] (S T : Set R) [(span S).IsTwoSided] :
span S * span T = span (S * T)
source
theorem Ideal.span_mul_span' {R : Type u} [Semiring R] (S T : Set R) [(span S).IsTwoSided] :
span S * span T = span (S * T)
source
theorem Ideal.span_singleton_mul_span_singleton {R : Type u} [Semiring R] (r s : R) [(span {r}).IsTwoSided] :
span {r} * span {s} = span {r * s}
source
theorem Ideal.span_singleton_pow {R : Type u} [Semiring R] (s : R) [(span {s}).IsTwoSided] (n : ℕ) :
span {s} ^ n = span {s ^ n}
source
theorem Ideal.mem_mul_span_singleton {R : Type u} [Semiring R] {x y : R} {I : Ideal R} [I.IsTwoSided] :
x ∈ I * span {y} ↔ ∃ z ∈ I, z * y = x
source
theorem Ideal.span_singleton_mul_left_mono {R : Type u} [Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R} (hx : x ≠ 0) :
I * span {x} ≤ J * span {x} ↔ I ≤ J
source
theorem Ideal.span_singleton_mul_left_inj {R : Type u} [Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R} (hx : x ≠ 0) :
I * span {x} = J * span {x} ↔ I = J
source
theorem Ideal.mul_le_inf {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] :
I * J ≤ I ⊓ J
source
theorem Ideal.sup_mul_eq_of_coprime_left {R : Type u} [Semiring R] {I J K : Ideal R} [I.IsTwoSided] (h : I ⊔ J = ⊤) :
I ⊔ J * K = I ⊔ K
source
theorem Ideal.sup_mul_eq_of_coprime_right {R : Type u} [Semiring R] {I J K : Ideal R} [J.IsTwoSided] (h : I ⊔ K = ⊤) :
I ⊔ J * K = I ⊔ J
source
theorem Ideal.mul_sup_eq_of_coprime_left {R : Type u} [Semiring R] {I J K : Ideal R} [J.IsTwoSided] (h : I ⊔ J = ⊤) :
I * K ⊔ J = K ⊔ J
source
theorem Ideal.mul_sup_eq_of_coprime_right {R : Type u} [Semiring R] {I J K : Ideal R} [I.IsTwoSided] (h : K ⊔ J = ⊤) :
I * K ⊔ J = I ⊔ J
source
theorem Ideal.sup_iInf_eq_top {R : Type u} [Semiring R] {I : Ideal R} {ι : Type u_1} {s : Finset ι} {J : ι → Ideal R} [∀ (i : ι), (J i).IsTwoSided] (h : ∀ i ∈ s, I ⊔ J i = ⊤) :
I ⊔ ⨅ i ∈ s, J i = ⊤
source
theorem Ideal.iInf_sup_eq_top {R : Type u} [Semiring R] {I : Ideal R} {ι : Type u_1} {s : Finset ι} {J : ι → Ideal R} [∀ (i : ι), (J i).IsTwoSided] (h : ∀ i ∈ s, J i ⊔ I = ⊤) :
(⨅ i ∈ s, J i) ⊔ I = ⊤
source
theorem Ideal.sup_pow_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) :
I ⊔ J ^ n = ⊤
source
theorem Ideal.sup_pow_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) :
I ⊔ J ^ n = ⊤
source
theorem Ideal.pow_sup_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) :
I ^ n ⊔ J = ⊤
source
theorem Ideal.pow_sup_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) :
I ^ n ⊔ J = ⊤
source
theorem Ideal.pow_sup_pow_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {m n : ℕ} (h : I ⊔ J = ⊤) :
I ^ m ⊔ J ^ n = ⊤
source
theorem Ideal.pow_sup_pow_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {m n : ℕ} (h : I ⊔ J = ⊤) :
I ^ m ⊔ J ^ n = ⊤
source
@[simp]
theorem Ideal.mul_top {R : Type u} [Semiring R] (I : Ideal R) [I.IsTwoSided] :
I * ⊤ = I
source
theorem Ideal.span_pair_mul_span_pair {R : Type u} [Semiring R] (w x y z : R) [(span {w, x}).IsTwoSided] :
span {w, x} * span {y, z} = span {w * y, w * z, x * y, x * z}
source
theorem Ideal.top_pow (R : Type u) [Semiring R] (n : ℕ) :
⊤ ^ n = ⊤
source
@[simp]
theorem Ideal.pow_eq_top_iff {R : Type u} [Semiring R] {I : Ideal R} {n : ℕ} :
I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0
source
theorem Ideal.natCast_eq_top {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) :
↑n = ⊤
source
theorem Ideal.ofNat_eq_top {R : Type u} [Semiring R] {n : ℕ} [n.AtLeastTwo] :
OfNat.ofNat n = ⊤

`3 : Ideal R` is not the ideal generated by 3 (which would be spelt `Ideal.span {3}`), it is simply `1 + 1 + 1 = ⊤`.

source
theorem Ideal.pow_eq_zero_of_mem {R : Type u} [Semiring R] {I : Ideal R} {n m : ℕ} (hnI : I ^ n = 0) (hmn : n ≤ m) {x : R} (hx : x ∈ I) :
x ^ m = 0
source
theorem Ideal.mul_mem_mul_rev {R : Type u} [CommSemiring R] {I J : Ideal R} {r s : R} (hr : r ∈ I) (hs : s ∈ J) :
s * r ∈ I * J
source
theorem Ideal.prod_mem_prod {R : Type u} [CommSemiring R] {ι : Type u_2} {s : Finset ι} {I : ι → Ideal R} {x : ι → R} :
(∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i
source
theorem Ideal.sup_pow_add_le_pow_sup_pow {R : Type u} [CommSemiring R] {I J : Ideal R} {n m : ℕ} :
(I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m
source
theorem Ideal.mul_comm {R : Type u} [CommSemiring R] (I J : Ideal R) :
I * J = J * I
source
theorem Ideal.mem_span_singleton_mul {R : Type u} [CommSemiring R] {x y : R} {I : Ideal R} :
x ∈ span {y} * I ↔ ∃ z ∈ I, y * z = x
source
@[simp]
theorem Ideal.range_mul {R : Type u} [CommSemiring R] (A : Type u_2) [CommSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) :
LinearMap.range ((LinearMap.mul R A) a) = Submodule.restrictScalars R (span {a})
source
theorem Ideal.range_mul' {R : Type u} [CommSemiring R] (a : R) :
LinearMap.range ((LinearMap.mul R R) a) = span {a}
source
theorem Ideal.le_span_singleton_mul_iff {R : Type u} [CommSemiring R] {x : R} {I J : Ideal R} :
I ≤ span {x} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
source
theorem Ideal.span_singleton_mul_le_iff {R : Type u} [CommSemiring R] {x : R} {I J : Ideal R} :
span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
source
theorem Ideal.span_singleton_mul_le_span_singleton_mul {R : Type u} [CommSemiring R] {x y : R} {I J : Ideal R} :
span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ
source
theorem Ideal.span_singleton_mul_right_mono {R : Type u} [CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R} (hx : x ≠ 0) :
span {x} * I ≤ span {x} * J ↔ I ≤ J
source
theorem Ideal.span_singleton_mul_right_inj {R : Type u} [CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R} (hx : x ≠ 0) :
span {x} * I = span {x} * J ↔ I = J
source
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) => span {x} * x_1
source
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 * span {x}
source
theorem Ideal.eq_span_singleton_mul {R : Type u} [CommSemiring R] {x : R} (I J : Ideal R) :
I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
source
theorem Ideal.span_singleton_mul_eq_span_singleton_mul {R : Type u} [CommSemiring R] {x y : R} (I J : Ideal R) :
span {x} * I = span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ
source
theorem Ideal.prod_span {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → Set R) :
∏ i ∈ s, span (I i) = span (∏ i ∈ s, I i)
source
theorem Ideal.prod_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R) :
∏ i ∈ s, span {I i} = span {∏ i ∈ s, I i}
source
@[simp]
theorem Ideal.multiset_prod_span_singleton {R : Type u} [CommSemiring R] (m : Multiset R) :
(Multiset.map (fun (x : R) => span {x}) m).prod = span {m.prod}
source
theorem Ideal.finset_inf_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R) (hI : (↑s).Pairwise (Function.onFun IsCoprime I)) :
(s.inf fun (i : ι) => span {I i}) = span {∏ i ∈ s, I i}
source
theorem Ideal.iInf_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} [Fintype ι] {I : ι → R} (hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)) :
⨅ (i : ι), span {I i} = span {∏ i : ι, I i}
source
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 : ι), span {↑(I i)} = span {↑(∏ i : ι, I i)}
source
theorem Ideal.sup_eq_top_iff_isCoprime {R : Type u_2} [CommSemiring R] (x y : R) :
span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y
source
theorem Ideal.multiset_prod_le_inf {R : Type u} [CommSemiring R] {s : Multiset (Ideal R)} :
s.prod ≤ s.inf
source
theorem Ideal.prod_le_inf {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} :
s.prod f ≤ s.inf f
source
theorem Ideal.mul_eq_inf_of_coprime {R : Type u} [CommSemiring R] {I J : Ideal R} (h : I ⊔ J = ⊤) :
I * J = I ⊓ J
source
theorem Ideal.sup_prod_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ι → Ideal R} (h : ∀ i ∈ s, I ⊔ J i = ⊤) :
I ⊔ ∏ i ∈ s, J i = ⊤
source
theorem Ideal.sup_multiset_prod_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} {s : Multiset (Ideal R)} (h : ∀ p ∈ s, I ⊔ p = ⊤) :
I ⊔ s.prod = ⊤
source
theorem Ideal.prod_sup_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ι → Ideal R} (h : ∀ i ∈ s, J i ⊔ I = ⊤) :
(∏ i ∈ s, J i) ⊔ I = ⊤
source
@[simp]
theorem Ideal.multiset_prod_eq_bot {R : Type u_2} [CommSemiring 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.

source
theorem Ideal.isCoprime_iff_codisjoint {R : Type u} [CommSemiring R] {I J : Ideal R} :
IsCoprime I J ↔ Codisjoint I J
source
theorem Ideal.isCoprime_of_isMaximal {R : Type u} [CommSemiring R] {I J : Ideal R} [I.IsMaximal] [J.IsMaximal] (ne : I ≠ J) :
IsCoprime I J
source
theorem Ideal.isCoprime_iff_add {R : Type u} [CommSemiring R] {I J : Ideal R} :
IsCoprime I J ↔ I + J = 1
source
theorem Ideal.isCoprime_iff_exists {R : Type u} [CommSemiring R] {I J : Ideal R} :
IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
source
theorem Ideal.isCoprime_iff_sup_eq {R : Type u} [CommSemiring R] {I J : Ideal R} :
IsCoprime I J ↔ I ⊔ J = ⊤
source
theorem Ideal.coprime_of_no_prime_ge {R : Type u} [CommSemiring R] {I J : Ideal R} (h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime) :
IsCoprime I J
source
theorem Ideal.isCoprime_tfae {R : Type u} [CommSemiring R] {I J : Ideal R} :
[IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE
source
theorem IsCoprime.codisjoint {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) :
Codisjoint I J
source
theorem IsCoprime.add_eq {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) :
I + J = 1
source
theorem IsCoprime.exists {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) :
∃ i ∈ I, ∃ j ∈ J, i + j = 1
source
theorem IsCoprime.sup_eq {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) :
I ⊔ J = ⊤
source
theorem Ideal.inf_eq_mul_of_isCoprime {R : Type u} [CommSemiring R] {I J : Ideal R} (coprime : IsCoprime I J) :
I ⊓ J = I * J
source
theorem Ideal.isCoprime_span_singleton_iff {R : Type u} [CommSemiring R] (x y : R) :
IsCoprime (span {x}) (span {y}) ↔ IsCoprime x y
source
theorem Ideal.isCoprime_biInf {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {J : ι → Ideal R} {s : Finset ι} (hf : ∀ j ∈ s, IsCoprime I (J j)) :
IsCoprime I (⨅ j ∈ s, J j)
source
def Ideal.radical {R : Type u} [CommSemiring R] (I : Ideal R) :
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

source
theorem Ideal.mem_radical_iff {R : Type u} [CommSemiring R] {I : Ideal R} {r : R} :
r ∈ I.radical ↔ ∃ (n : ℕ), r ^ n ∈ I
source
def Ideal.IsRadical {R : Type u} [CommSemiring R] (I : Ideal R) :
Prop

An ideal is radical if it contains its radical.

Equations

- I.IsRadical = (I.radical ≤ I)

Instances For

source
theorem Ideal.le_radical {R : Type u} [CommSemiring R] {I : Ideal R} :
I ≤ I.radical
source
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.

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

Alias of the reverse direction of `Ideal.radical_eq_iff`.

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

source
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 ∈ I → r ∈ I
source
theorem Ideal.radical_top (R : Type u) [CommSemiring R] :
⊤.radical = ⊤
source
theorem Ideal.radical_mono {R : Type u} [CommSemiring R] {I J : Ideal R} (H : I ≤ J) :
I.radical ≤ J.radical
source
theorem Ideal.radical_isRadical {R : Type u} [CommSemiring R] (I : Ideal R) :
I.radical.IsRadical
source
@[simp]
theorem Ideal.radical_idem {R : Type u} [CommSemiring R] (I : Ideal R) :
I.radical.radical = I.radical
source
theorem Ideal.IsRadical.radical_le_iff {R : Type u} [CommSemiring R] {I J : Ideal R} (hJ : J.IsRadical) :
I.radical ≤ J ↔ I ≤ J
source
theorem Ideal.radical_le_radical_iff {R : Type u} [CommSemiring R] {I J : Ideal R} :
I.radical ≤ J.radical ↔ I ≤ J.radical
source
theorem Ideal.radical_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} :
I.radical = ⊤ ↔ I = ⊤
source
theorem Ideal.IsPrime.isRadical {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) :
I.IsRadical
source
theorem Ideal.IsPrime.radical {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) :
I.radical = I
source
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
source
theorem Ideal.disjoint_powers_iff_notMem {R : Type u} [CommSemiring R] {I : Ideal R} (y : R) (hI : I.IsRadical) :
Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I.toAddSubmonoid
source
@[deprecated Ideal.disjoint_powers_iff_notMem (since := "2025-05-23")]
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 ↔ y ∉ I.toAddSubmonoid

Alias of `Ideal.disjoint_powers_iff_notMem`.

source
theorem Ideal.radical_sup {R : Type u} [CommSemiring R] (I J : Ideal R) :
(I ⊔ J).radical = (I.radical ⊔ J.radical).radical
source
theorem Ideal.radical_inf {R : Type u} [CommSemiring R] (I J : Ideal R) :
(I ⊓ J).radical = I.radical ⊓ J.radical
source
theorem Ideal.IsRadical.inf {R : Type u} [CommSemiring R] {I J : Ideal R} (hI : I.IsRadical) (hJ : J.IsRadical) :
(I ⊓ J).IsRadical
source
theorem Ideal.isRadical_bot_iff {R : Type u} [CommSemiring R] :
⊥.IsRadical ↔ IsReduced R
source
theorem Ideal.isRadical_bot {R : Type u} [CommSemiring R] [IsReduced R] :
⊥.IsRadical
source
def Ideal.radicalInfTopHom {R : Type u} [CommSemiring R] :
InfTopHom (Ideal R) (Ideal R)

`Ideal.radical` as an `InfTopHom`, bundling in that it distributes over `inf`.

Equations

- Ideal.radicalInfTopHom = { toFun := Ideal.radical, map_inf' := ⋯, map_top' := ⋯ }

Instances For

source
@[simp]
theorem Ideal.radicalInfTopHom_apply {R : Type u} [CommSemiring R] (I : Ideal R) :
radicalInfTopHom I = I.radical
source
theorem Ideal.radical_finset_inf {R : Type u} [CommSemiring R] {ι : Type u_2} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) :
(s.inf f).radical = (f i).radical
source
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 : ℤ)}`.

source
theorem Ideal.isRadical_iInf {R : Type u} [CommSemiring R] {ι : Sort u_2} (I : ι → Ideal R) (hI : ∀ (i : ι), (I i).IsRadical) :
(⨅ (i : ι), I i).IsRadical
source
theorem Ideal.radical_mul {R : Type u} [CommSemiring R] (I J : Ideal R) :
(I * J).radical = I.radical ⊓ J.radical
source
theorem Ideal.IsPrime.radical_le_iff {R : Type u} [CommSemiring R] {I J : Ideal R} (hJ : J.IsPrime) :
I.radical ≤ J ↔ I ≤ J
source
theorem Ideal.radical_eq_sInf {R : Type u} [CommSemiring R] (I : Ideal R) :
I.radical = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
source
theorem Ideal.isRadical_bot_of_noZeroDivisors {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] :
⊥.IsRadical
source
@[simp]
theorem Ideal.radical_bot_of_noZeroDivisors {R : Type u} [CommSemiring R] [NoZeroDivisors R] :
⊥.radical = ⊥
source
instance Ideal.instIdemCommSemiring {R : Type u} [CommSemiring R] :
IdemCommSemiring (Ideal R)
Equations

- Ideal.instIdemCommSemiring = inferInstance

source
theorem Ideal.radical_pow {R : Type u} [CommSemiring R] (I : Ideal R) {n : ℕ} :
n ≠ 0 → (I ^ n).radical = I.radical
source
theorem Ideal.IsPrime.mul_le {R : Type u} [CommSemiring R] {I J P : Ideal R} (hp : P.IsPrime) :
I * J ≤ P ↔ I ≤ P ∨ J ≤ P
source
theorem Ideal.IsPrime.inf_le {R : Type u} [CommSemiring R] {I J P : Ideal R} (hp : P.IsPrime) :
I ⊓ J ≤ P ↔ I ≤ P ∨ J ≤ P
source
theorem Ideal.IsPrime.multiset_prod_le {R : Type u} [CommSemiring R] {s : Multiset (Ideal R)} {P : Ideal R} (hp : P.IsPrime) :
s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P
source
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 ↔ ∃ i ∈ s, f i ≤ P
source
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 ↔ ∃ p ∈ s, p ∈ I
source
theorem Ideal.IsPrime.pow_le_iff {R : Type u} [CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (hn : n ≠ 0) :
I ^ n ≤ P ↔ I ≤ P
source
theorem Ideal.IsPrime.le_of_pow_le {R : Type u} [CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (h : I ^ n ≤ P) :
I ≤ P
source
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 ↔ ∃ i ∈ s, f i ≤ P
source
theorem Ideal.IsPrime.prod_mem_iff {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {x : ι → R} {p : Ideal R} [hp : p.IsPrime] :
∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

The product of a finite number of elements in the commutative semiring `R` lies in the prime ideal `p` if and only if at least one of those elements is in `p`.

source
theorem Ideal.IsPrime.prod_mem_iff_exists_mem {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Finset R) :
∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I
source
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 ↔ ∃ i ∈ s, f i ≤ P
source
theorem Ideal.subset_union {R : Type u} [Ring R] {I J K : Ideal R} :
↑I ⊆ ↑J ∪ ↑K ↔ I ≤ J ∨ I ≤ K
source
theorem Ideal.subset_union_prime' {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} {a b : ι} (hp : ∀ i ∈ s, (f i).IsPrime) {I : Ideal R} :
↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) ↔ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
source
theorem Ideal.subset_union_prime {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} (a b : ι) (hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) {I : Ideal R} :
↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

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

source
theorem Ideal.subset_union_prime_finite {R : Type u_2} {ι : Type u_3} [CommRing R] {s : Set ι} (hs : s.Finite) {f : ι → Ideal R} (a b : ι) (hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) {I : Ideal R} :
↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Another version of prime avoidance using `Set.Finite` instead of `Finset`.

source
theorem Ideal.le_of_dvd {R : Type u} [CommSemiring R] {I J : Ideal R} :
I ∣ J → J ≤ I

If `I` divides `J`, then `I` contains `J`.

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

source
@[simp]
theorem Ideal.dvd_bot {R : Type u} [CommSemiring R] {I : Ideal R} :
I ∣ ⊥
source
@[simp]
theorem Ideal.isUnit_iff {R : Type u} [CommSemiring R] {I : Ideal R} :
IsUnit I ↔ I = ⊤

See also `isUnit_iff_eq_one`.

source
instance Ideal.uniqueUnits {R : Type u} [CommSemiring R] :
Unique (Ideal R)ˣ
Equations

- Ideal.uniqueUnits = { default := 1, uniq := ⋯ }

source
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.linearCombination` that takes in vectors valued in `I`.

Equations

- Ideal.finsuppTotal ι M I v = Finsupp.linearCombination R v ∘ₗ Finsupp.mapRange.linearMap (Submodule.subtype I)

Instances For

source
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) :
(finsuppTotal ι M I v) f = f.sum fun (i : ι) (x : ↥I) => ↑x • v i
source
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) :
(finsuppTotal ι M I v) f = ∑ i : ι, ↑(f i) • v i
source
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} :
LinearMap.range (finsuppTotal ι M I v) = I • Submodule.span R (Set.range v)
source
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
source
theorem Ideal.mem_span_range_iff_exists_fun {α : Type u_1} {R : Type u_2} [Semiring R] [Fintype α] {x : R} {v : α → R} :
x ∈ 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`.

source
theorem Associates.mk_ne_zero' {R : Type u_1} [CommSemiring R] {r : R} :
Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0
source
theorem Ideal.span_singleton_nonZeroDivisors {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {r : R} :
span {r} ∈ nonZeroDivisors (Ideal R) ↔ r ∈ nonZeroDivisors R
source
theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] (P : Ideal R) [P.IsPrime] :
P.primeCompl ≤ nonZeroDivisors R
source
instance Submodule.moduleSubmodule {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
Module (Ideal R) (Submodule R M)
Equations

- Submodule.moduleSubmodule = { toSMul := Submodule.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
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) :
Ideal.span s • N = s • N
source
@[simp]
theorem Submodule.set_smul_top_eq_span {R : Type u} [CommSemiring R] (s : Set R) :
s • ⊤ = Ideal.span s
source
theorem Submodule.smul_le_span {R : Type u} [CommSemiring R] (s : Set R) (I : Ideal R) :
s • I ≤ Ideal.span s
source
instance Submodule.algebraIdeal {R : Type u} [CommSemiring R] {A : Type u_1} [Semiring A] [Algebra R A] :
Algebra (Ideal R) (Submodule R A)
Equations

- One or more equations did not get rendered due to their size.

source
def Submodule.mapAlgHom {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
Submodule R A →ₐ[Ideal R] Submodule R B

`Submonoid.map` as an `AlgHom`, when applied to an `AlgHom`.

Equations

- Submodule.mapAlgHom f = { toRingHom := Submodule.mapHom f, commutes' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.coe_mapAlgHom_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (p : Submodule R A) :
↑((mapAlgHom f) p) = ⇑f '' ↑p
source
def Submodule.mapAlgEquiv {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :
Submodule R A ≃ₐ[Ideal R] Submodule R B

`Submonoid.map` as an `AlgEquiv`, when applied to an `AlgEquiv`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Submodule.coe_mapAlgEquiv_symm_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (a : Submodule R B) :
↑((mapAlgEquiv f).symm a) = (fun (a : B) => f.symm a) '' ↑a
source
@[simp]
theorem Submodule.coe_mapAlgEquiv_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (a✝ : Submodule R A) :
↑((mapAlgEquiv f) a✝) = (fun (a : A) => f a) '' ↑a✝
source
instance instNonUnitalSubsemiringClassIdeal {R : Type u_1} [Semiring R] :
NonUnitalSubsemiringClass (Ideal R) R
source
instance instNonUnitalSubringClassIdeal {R : Type u_1} [Ring R] :
NonUnitalSubringClass (Ideal R) R
source
theorem Ideal.exists_subset_radical_span_sup_of_subset_radical_sup {R : Type u_1} [CommSemiring R] (s : Set R) (I J : Ideal R) (hs : s ⊆ ↑(I ⊔ J).radical) :
∃ (t : ↑s → R), Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical
source
@[deprecated Ideal.exists_subset_radical_span_sup_of_subset_radical_sup (since := "2025-05-13")]
theorem Ideal.exists_subset_radical_span_sup_span_of_subset_radical_sup {R : Type u_1} [CommSemiring R] (s : Set R) (I J : Ideal R) (hs : s ⊆ ↑(I ⊔ J).radical) :
∃ (t : ↑s → R), Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical

Alias of `Ideal.exists_subset_radical_span_sup_of_subset_radical_sup`.