Commit 2026-05-16 09:13 ce47089f
View on Github →feat(RingTheory/Ideal/Operations): Generalized span_singleton_toAddSubgroup_eq_zmultiples (#39453)
The previous version of span_singleton_toAddSubgroup_eq_zmultiples worked only for (a : ℤ). It can be easily generalized to (a : M) for any [AddCommGroup M] with minimal changes to the proof and zero downstream breakage.