Theorems · Theorem · commutative algebra

DividedPowers.SubDPIdeal.span_carrier_eq_dpow_span

∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {S : Set A},
  S ⊆ ↑I →
    (DividedPowers.SubDPIdeal.span hI S).carrier =
      Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

The underlying ideal of SubDPIdeal.span hI S is generated by the elements of the form hI.dpow n x with n > 0 and x ∈ S.

Defined in

Mathlib.RingTheory.DividedPowers.SubDPIdeal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiring