Commit 2024-02-14 00:27 6f21dbda
View on Github →chore: Split off getD/getI lemmas from Data.List.Basic (#10337) Splits off some lemmas from the end of this file, reducing the size of what is currently the longest file in mathlib.
chore: Split off getD/getI lemmas from Data.List.Basic (#10337) Splits off some lemmas from the end of this file, reducing the size of what is currently the longest file in mathlib.