Theorem Ideal.span_mul_span'

Modification history

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 →