Commit 2025-10-28 10:18 50818a51

View on Github →

feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg (#22151) A key fact used is Module.FG.smul: if I is a two-sided ideal of R that is f.g. as a left ideal and N is a f.g. R-module, then I • M is also a f.g. R-module. Many lemmas about coprimality of ideals are also generalized to the noncommutative, two-sided setting.

Estimated changes

added theorem Ideal.fg_top
added theorem Ideal.FG.mul
added theorem Ideal.FG.pow
added theorem Submodule.FG.smul
modified theorem Ideal.iInf_sup_eq_top
modified theorem Ideal.mul_le_inf
modified theorem Ideal.mul_top
modified theorem Ideal.natCast_eq_top
added theorem Ideal.pow_sup_eq_top'
modified theorem Ideal.pow_sup_eq_top
modified theorem Ideal.pow_sup_pow_eq_top
modified theorem Ideal.span_mul_span'
modified theorem Ideal.span_mul_span
modified theorem Ideal.span_singleton_pow
modified theorem Ideal.sup_iInf_eq_top
added theorem Ideal.sup_pow_eq_top'
modified theorem Ideal.sup_pow_eq_top
modified theorem Submodule.span_smul_span