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.

Estimated changes

deleted theorem List.getD_append
deleted theorem List.getD_append_right
deleted theorem List.getD_cons_succ
deleted theorem List.getD_cons_zero
deleted theorem List.getD_default_eq_getI
deleted theorem List.getD_eq_default
deleted theorem List.getD_eq_get
deleted theorem List.getD_eq_getD_get?
deleted theorem List.getD_eq_nthLe
deleted theorem List.getD_map
deleted theorem List.getD_nil
deleted theorem List.getI_append
deleted theorem List.getI_append_right
deleted theorem List.getI_cons_succ
deleted theorem List.getI_cons_zero
deleted theorem List.getI_eq_default
deleted theorem List.getI_eq_get
deleted theorem List.getI_eq_iget_get?
deleted theorem List.getI_eq_nthLe
deleted theorem List.getI_nil
deleted theorem List.getI_zero_eq_headI
added theorem List.getD_append
added theorem List.getD_append_right
added theorem List.getD_cons_succ
added theorem List.getD_cons_zero
added theorem List.getD_eq_default
added theorem List.getD_eq_get
added theorem List.getD_eq_getD_get?
added theorem List.getD_eq_nthLe
added theorem List.getD_map
added theorem List.getD_nil
added theorem List.getI_append
added theorem List.getI_append_right
added theorem List.getI_cons_succ
added theorem List.getI_cons_zero
added theorem List.getI_eq_default
added theorem List.getI_eq_get
added theorem List.getI_eq_iget_get?
added theorem List.getI_eq_nthLe
added theorem List.getI_nil