Theorems · Theorem · commutative algebra

Ideal.span_prod

∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {s : Set R} {t : Set S},
  (s.Nonempty ↔ t.Nonempty) → Ideal.span (s ×ˢ t) = (Ideal.span s).prod (Ideal.span t)

Defined in

Mathlib.RingTheory.Ideal.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringSemiring