Commit 2024-11-13 20:45 c6e93f50
View on Github →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.