More operations on modules and ideals

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

theorem Submodule.span_singleton_toAddSubgroup_eq_zmultiples (a : ℤ) : (ℤ ∙ a).toAddSubgroup = AddSubgroup.zmultiples a

@[simp]

theorem Ideal.span_singleton_toAddSubgroup_eq_zmultiples (a : ℤ) : Submodule.toAddSubgroup (span {a}) = AddSubgroup.zmultiples a

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.

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

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 • ⊤

@[simp]

theorem Submodule.top_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : ⊤ • N = N

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

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'

@[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

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

@[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)

theorem Submodule.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'} (hf : Function.Injective ⇑f) {p : Submodule R M'} (hp : p ≤ f.range) {I : Ideal R} : comap f (I • p) = I • comap f p

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 • (R ∙ m) ↔ ∃ y ∈ I, y • m = x

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)

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)

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.

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

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

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_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_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

@[simp]

theorem Ideal.add_eq_sup {R : Type u} [Semiring R] {I 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

@[simp]

theorem Ideal.one_eq_top {R : Type u} [Semiring R] : 1 = ⊤

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

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

theorem Ideal.bot_pow {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : ⊥ ^ n = ⊥

theorem Ideal.pow_mem_pow {R : Type u} [Semiring R] {I : Ideal R} {x : R} (hx : x ∈ I) (n : ℕ) : x ^ n ∈ I ^ n

theorem Ideal.mul_le {R : Type u} [Semiring R] {I J K : Ideal R} : I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K

theorem Ideal.mul_le_left {R : Type u} [Semiring R] {I J : Ideal R} : I * J ≤ J

@[simp]

theorem Ideal.sup_mul_left_self {R : Type u} [Semiring R] {I J : Ideal R} : I ⊔ J * I = I

@[simp]

theorem Ideal.mul_left_self_sup {R : Type u} [Semiring R] {I J : Ideal R} : J * I ⊔ I = I

theorem Ideal.mul_le_right {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I * J ≤ I

@[simp]

theorem Ideal.sup_mul_right_self {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I ⊔ I * J = I

@[simp]

theorem Ideal.mul_right_self_sup {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I * J ⊔ I = I

theorem Ideal.mul_assoc {R : Type u} [Semiring R] {I J K : Ideal R} : I * J * K = I * (J * K)

theorem Ideal.mul_bot {R : Type u} [Semiring R] (I : Ideal R) : I * ⊥ = ⊥

theorem Ideal.bot_mul {R : Type u} [Semiring R] (I : Ideal R) : ⊥ * I = ⊥

@[simp]

theorem Ideal.top_mul {R : Type u} [Semiring R] (I : Ideal R) : ⊤ * I = I

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

theorem Ideal.mul_mono_left {R : Type u} [Semiring R] {I J K : Ideal R} (h : I ≤ J) : I * K ≤ J * K

theorem Ideal.mul_mono_right {R : Type u} [Semiring R] {I J K : Ideal R} (h : J ≤ K) : I * J ≤ I * K

theorem Ideal.mul_sup {R : Type u} [Semiring R] (I J K : Ideal R) : I * (J ⊔ K) = I * J ⊔ I * K

theorem Ideal.sup_mul {R : Type u} [Semiring R] (I J K : Ideal R) : (I ⊔ J) * K = I * K ⊔ J * K

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

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

theorem Ideal.pow_le_pow_right {R : Type u} [Semiring R] {I : Ideal R} {m n : ℕ} (h : m ≤ n) : I ^ n ≤ I ^ m

theorem Ideal.pow_le_self {R : Type u} [Semiring R] {I : Ideal R} {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ I

theorem Ideal.pow_right_mono {R : Type u} [Semiring R] {I J : Ideal R} (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n

@[instance 100]

instance Ideal.IsTwoSided.instHMul {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] : (I * J).IsTwoSided

@[instance 100]

instance Ideal.IsTwoSided.instHPowNat {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ) : (I ^ n).IsTwoSided

theorem Ideal.IsTwoSided.mul_one {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] : I * 1 = I

theorem Ideal.IsTwoSided.pow_add {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (m n : ℕ) : I ^ (m + n) = I ^ m * I ^ n

theorem Ideal.IsTwoSided.pow_succ {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ) : I ^ (n + 1) = I * I ^ n

@[simp]

theorem Ideal.mul_eq_bot {R : Type u} [Semiring R] {I J : Ideal R} [NoZeroDivisors R] : I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥

instance Ideal.instNoZeroDivisors {R : Type u} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R)

instance Ideal.instIsTorsionFreeSubtypeMemSubmodule {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] [Module.IsTorsionFree R A] {I : Submodule S A} : Module.IsTorsionFree R ↥I

theorem Ideal.span_mul_span {R : Type u} [Semiring R] (S T : Set R) [(span S).IsTwoSided] : span S * span T = span (S * T)

theorem Ideal.span_mul_span' {R : Type u} [Semiring R] (S T : Set R) [(span S).IsTwoSided] : span S * span T = span (S * T)

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}

theorem Ideal.span_singleton_pow {R : Type u} [Semiring R] (s : R) [(span {s}).IsTwoSided] (n : ℕ) : span {s} ^ n = span {s ^ n}

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

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

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

theorem Ideal.mul_le_inf {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I * J ≤ I ⊓ J

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

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

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

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

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 = ⊤

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 = ⊤

theorem Ideal.sup_pow_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ⊔ J ^ n = ⊤

theorem Ideal.sup_pow_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ⊔ J ^ n = ⊤

theorem Ideal.pow_sup_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ^ n ⊔ J = ⊤

theorem Ideal.pow_sup_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ^ n ⊔ J = ⊤

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 = ⊤

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 = ⊤

@[simp]

theorem Ideal.mul_top {R : Type u} [Semiring R] (I : Ideal R) [I.IsTwoSided] : I * ⊤ = I

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}

theorem Ideal.top_pow (R : Type u) [Semiring R] (n : ℕ) : ⊤ ^ n = ⊤

@[simp]

theorem Ideal.pow_eq_top_iff {R : Type u} [Semiring R] {I : Ideal R} {n : ℕ} : I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0

theorem Ideal.natCast_eq_top {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : ↑n = ⊤

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 = ⊤.

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

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

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

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

theorem Ideal.mul_comm {R : Type u} [CommSemiring R] (I J : Ideal R) : I * J = J * I

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

@[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.mul R A) a).range = Submodule.restrictScalars R (span {a})

theorem Ideal.range_mul' {R : Type u} [CommSemiring R] (a : R) : ((LinearMap.mul R R) a).range = span {a}

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

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

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

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

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

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

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}

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

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

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)

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}

@[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}

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}

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}

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)}

theorem Ideal.sup_eq_top_iff_isCoprime {R : Type u_2} [CommSemiring R] (x y : R) : span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y

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 J : Ideal R} (h : I ⊔ J = ⊤) : I * 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 : ∀ i ∈ s, I ⊔ J i = ⊤) : I ⊔ ∏ i ∈ s, J i = ⊤

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 = ⊤

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 = ⊤

@[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.

theorem Ideal.isCoprime_iff_codisjoint {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ Codisjoint I J

theorem Ideal.isCoprime_of_isMaximal {R : Type u} [CommSemiring R] {I J : Ideal R} [I.IsMaximal] [J.IsMaximal] (ne : I ≠ J) : IsCoprime I J

theorem Ideal.isCoprime_iff_add {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ I + J = 1

theorem Ideal.isCoprime_iff_exists {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

theorem Ideal.isCoprime_iff_sup_eq {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ I ⊔ J = ⊤

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

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

theorem IsCoprime.codisjoint {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : Codisjoint I J

theorem IsCoprime.add_eq {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : I + J = 1

theorem IsCoprime.exists {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : ∃ i ∈ I, ∃ j ∈ J, i + j = 1

theorem IsCoprime.sup_eq {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : I ⊔ J = ⊤

theorem Ideal.isCoprime_span_singleton_iff {R : Type u} [CommSemiring R] (x y : R) : IsCoprime (span {x}) (span {y}) ↔ IsCoprime x y

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)

theorem Ideal.mul_eq_inf_of_isCoprime {R : Type u} [CommSemiring R] {I J : Ideal R} (coprime : IsCoprime I J) : I * J = I ⊓ J

@[deprecated Ideal.mul_eq_inf_of_isCoprime (since := "2026-03-10")]

theorem Ideal.inf_eq_mul_of_isCoprime {R : Type u} [CommSemiring R] {I J : Ideal R} (coprime : IsCoprime I J) : I ⊓ J = I * J

theorem Ideal.prod_eq_iInf_of_pairwise_isCoprime {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {J : ι → Ideal R} (hp : (↑s).Pairwise (Function.onFun IsCoprime J)) : ∏ i ∈ s, J i = ⨅ i ∈ s, J i

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.

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) : Prop

An ideal is radical if it contains its radical.

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.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.

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

theorem Ideal.radical_top (R : Type u) [CommSemiring R] : ⊤.radical = ⊤

theorem Ideal.radical_mono {R : Type u} [CommSemiring R] {I 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 J : Ideal R} (hJ : J.IsRadical) : I.radical ≤ J ↔ I ≤ J

theorem Ideal.radical_le_radical_iff {R : Type u} [CommSemiring R] {I J : Ideal R} : I.radical ≤ J.radical ↔ I ≤ J.radical

@[simp]

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_notMem {R : Type u} [CommSemiring R] {I : Ideal R} (y : R) (hI : I.IsRadical) : Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I.toAddSubmonoid

theorem Ideal.radical_sup {R : Type u} [CommSemiring R] (I J : Ideal R) : (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

theorem Ideal.radical_inf {R : Type u} [CommSemiring R] (I J : Ideal R) : (I ⊓ J).radical = I.radical ⊓ J.radical

theorem Ideal.IsRadical.inf {R : Type u} [CommSemiring R] {I J : Ideal R} (hI : I.IsRadical) (hJ : J.IsRadical) : (I ⊓ J).IsRadical

theorem Ideal.isRadical_bot_iff {R : Type u} [CommSemiring R] : ⊥.IsRadical ↔ IsReduced R

theorem Ideal.isRadical_bot {R : Type u} [CommSemiring R] [IsReduced R] : ⊥.IsRadical

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.

@[simp]

theorem Ideal.radicalInfTopHom_apply {R : Type u} [CommSemiring R] (I : Ideal R) : radicalInfTopHom I = I.radical

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

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 J : Ideal R) : (I * J).radical = I.radical ⊓ J.radical

theorem Ideal.IsPrime.radical_le_iff {R : Type u} [CommSemiring R] {I 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}

theorem Ideal.isRadical_bot_of_noZeroDivisors {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] : ⊥.IsRadical

@[simp]

theorem Ideal.radical_bot_of_noZeroDivisors {R : Type u} [CommSemiring R] [NoZeroDivisors R] : ⊥.radical = ⊥

@[implicit_reducible]

instance Ideal.instIdemCommSemiring {R : Type u} [CommSemiring R] : IdemCommSemiring (Ideal R)

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 J P : Ideal R} (hp : P.IsPrime) : I * J ≤ P ↔ I ≤ P ∨ J ≤ P

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

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

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

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

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

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

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

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.

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

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

theorem Ideal.eq_inf_of_isPrime_inf {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} (hp : (s.inf f).IsPrime) : ∃ i ∈ s, f i = s.inf f

theorem Ideal.IsPrime.notMem_of_isCoprime_of_mem {R : Type u} [CommSemiring R] {I : Ideal R} [I.IsPrime] {x y : R} (h : IsCoprime x y) (hx : x ∈ I) : y ∉ I

theorem Ideal.subset_union {R : Type u} [Ring R] {I J 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 : ∀ 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

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.

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.

theorem Ideal.IsMaximal.exists_inv_pow {R : Type u} [CommSemiring R] (I : Ideal R) [I.IsMaximal] {x : R} (hx : x ∉ I) (n : ℕ) : ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1

Generalize Ideal.IsMaximal.exists_inv to power of maximal ideals.

theorem Ideal.IsMaximal.mul_mem_pow {R : Type u} [CommSemiring R] (I : Ideal R) [I.IsMaximal] {a b : R} {n : ℕ} (h : a * b ∈ I ^ n) : a ∈ I ∨ b ∈ I ^ n

See also Ideal.IsPrime.mul_mem_pow for prime ideal in Dedekind domain.

theorem Ideal.IsMaximal.mem_pow_mul {R : Type u_2} [CommSemiring R] (I : Ideal R) [I.IsMaximal] {a b : R} {n : ℕ} (h : a * b ∈ I ^ n) : a ∈ I ^ n ∨ b ∈ I

See also Ideal.IsPrime.mem_pow_mul for prime ideal in Dedekind domain.

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.

@[simp]

theorem Ideal.dvd_bot {R : Type u} [CommSemiring R] {I : Ideal R} : I ∣ ⊥

@[simp]

theorem Ideal.isUnit_iff {R : Type u} [CommSemiring R] {I : Ideal R} : IsUnit I ↔ I = ⊤

See also isUnit_iff_eq_one.

@[implicit_reducible]

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

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.

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

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

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} : (finsuppTotal ι M I v).range = I • Submodule.span R (Set.range v)

@[implicit_reducible]

noncomputable instance Ideal.instDecidableEqAssociates {R : Type u_1} [CommSemiring R] : DecidableEq (Associates (Ideal R))

Associates (Ideal R) almost never has decidable equality. We add a global instance that Associates (Ideal R) has decidable equality, coming from the choice axiom, so that we don't have to provide [DecidableEq (Associates (Ideal R))] arguments in lemma statements.

@[implicit_reducible]

noncomputable instance Ideal.instDecidableIrreducibleAssociates {R : Type u_1} [CommSemiring R] (I : Associates (Ideal R)) : Decidable (Irreducible I)

Associates (Ideal R) almost never has a decidable reducibility check. We add a global instance that members of Associates (Ideal R) have decidable reducibility, coming from the choice axiom, so that we don't have to provide this as an arguments in lemma statements.

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 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.

theorem Associates.mk_ne_zero' {R : Type u_1} [CommSemiring R] {r : R} : Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0

theorem Ideal.span_singleton_nonZeroDivisors {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {r : R} : span {r} ∈ nonZeroDivisors (Ideal R) ↔ r ∈ nonZeroDivisors R

theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] (P : Ideal R) [P.IsPrime] : P.primeCompl ≤ nonZeroDivisors R

@[implicit_reducible]

instance Submodule.moduleSubmodule {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] : Module (Ideal R) (Submodule R M)

theorem Submodule.span_smul_eq {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (s : Set R) (N : Submodule R M) : Ideal.span s • N = s • N

@[simp]

theorem Submodule.set_smul_top_eq_span {R : Type u_1} [CommSemiring R] (s : Set R) : s • ⊤ = Ideal.span s

theorem Submodule.smul_le_span {R : Type u_1} [CommSemiring R] (s : Set R) (I : Ideal R) : s • I ≤ Ideal.span s

@[implicit_reducible]

instance Submodule.algebraIdeal {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] : Algebra (Ideal R) (Submodule R A)

def Submodule.mapAlgHom {R : Type u_1} [CommSemiring R] {A : Type u_3} {B : Type u_4} [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.

@[simp]

theorem Submodule.coe_mapAlgHom_apply {R : Type u_1} [CommSemiring R] {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (p : Submodule R A) : ↑((mapAlgHom f) p) = ⇑f '' ↑p

def Submodule.mapAlgEquiv {R : Type u_1} [CommSemiring R] {A : Type u_3} {B : Type u_4} [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.

@[simp]

theorem Submodule.coe_mapAlgEquiv_symm_apply {R : Type u_1} [CommSemiring R] {A : Type u_3} {B : Type u_4} [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

@[simp]

theorem Submodule.coe_mapAlgEquiv_apply {R : Type u_1} [CommSemiring R] {A : Type u_3} {B : Type u_4} [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✝

theorem Submodule.smul_top_le_comap_smul_top {R : Type u_1} [Semiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (I : Ideal R) (f : M →ₗ[R] N) : I • ⊤ ≤ comap f (I • ⊤)

theorem Submodule.comap_smul_top_of_surjective {R : Type u_1} [Semiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (I : Ideal R) (f : M →ₗ[R] N) (h : Function.Surjective ⇑f) : comap f (I • ⊤) = I • ⊤ ⊔ f.ker

instance instNonUnitalSubsemiringClassIdeal {R : Type u_1} [Semiring R] : NonUnitalSubsemiringClass (Ideal R) R

instance instNonUnitalSubringClassIdeal {R : Type u_1} [Ring R] : NonUnitalSubringClass (Ideal R) R

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