Commit 2024-11-13 20:45 c6e93f50

feat(Algebra/Module/Submodule/Pointwise): span_singleton_toAddSubgroup_eq_zmultiples (#18965) Add lemmas equating the span of a single element of ℤ (Submodule.span or Ideal.span) to AddSubgroup.zmultiples. Extracted from #18002, where this location was suggested based on find_home rather than any stronger link to the other lemmas here (Mathlib.RingTheory.Ideal.Span doesn't know about zmultiples). Indirectly from AperiodicMonotilesLean after refactoring via #18002.