Theorem Ideal.span_mul_span'

Modification history

2026-08-14 20:33

Mathlib/RingTheory/Ideal/Operations.lean

chore(RingTheory/Ideal/Operations): deprecate duplicate theorem `Ideal.span_mul_span'` (#39799) …

Deleted Ideal.span_mul_span'View on Github →

2025-10-28 10:18

Mathlib/RingTheory/Ideal/Operations.lean

feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg (#22151) …

Modified Ideal.span_mul_span'View on Github →

2023-03-09 08:23

Mathlib/RingTheory/Ideal/Operations.lean

feat: port RingTheory.Ideal.Operations (#2701)

Added Ideal.span_mul_span'View on Github →