Theorems · Theorem · commutative algebra

Ideal.radical_finset_inf

∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} {s : Finset ι} {f : ι → Ideal R} {i : ι},
  i ∈ s → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).radical = (f i).radical

Defined in

Mathlib.RingTheory.Ideal.Operations

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiring