Commit 2025-01-13 11:54 2b47f631
View on Github →chore(Data/List): move a Prod lemma from Basic.lean to ProdSigma.lean (#20702)
Noticed in the late importers report: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Late.20importers.20report/near/493286162
List/Basic.lean is very low down in the hierarchy so saving a few imports here might cause a big change transitively.