Commit 2025-08-26 00:29 2a1d0836

View on Github →

feat: add lemmas about List.scanr (#26838) I add basic lemmas to reason about List.scanr, and slightly clean-up the file and add some basic lemmas to keep the API unified with the one for List.scanl. Original PR: https://github.com/leanprover-community/mathlib4/pull/25188

Estimated changes

added theorem List.drop_scanr
added theorem List.getElem?_scanr
modified theorem List.getElem_scanl_zero
added theorem List.getElem_scanr
added theorem List.head_scanl
added theorem List.head_scanr
modified theorem List.length_scanl
added theorem List.length_scanr
added theorem List.scanl_iff_nil
added theorem List.scanl_ne_nil
modified theorem List.scanl_nil
added theorem List.scanr_append
modified theorem List.scanr_cons
added theorem List.scanr_iff_nil
added theorem List.scanr_ne_nil
modified theorem List.scanr_nil
added theorem List.tail_scanr