Commit 2023-10-20 05:04 aa0ff04a

View on Github →

style: rename Stream'.nth to Stream'.get (#7514) Many of nth (e.g. list.nth, stream.seq.nth) are renamed to get? in Mathlib 4, but Stream'.nth had been remained as it.

Estimated changes

modified theorem Hindman.FP.singleton
added theorem Stream'.Seq.ofList_get
deleted theorem Stream'.Seq.ofList_nth
modified def Stream'.All
modified def Stream'.Any
modified def Stream'.apply
modified def Stream'.drop
modified def Stream'.enum
added def Stream'.get
modified def Stream'.map
deleted def Stream'.nth
modified def Stream'.tail
modified theorem Stream'.all_def
modified theorem Stream'.any_def
deleted theorem Stream'.concat_take_nth
modified theorem Stream'.get?_take
added theorem Stream'.get_const
added theorem Stream'.get_drop
added theorem Stream'.get_enum
added theorem Stream'.get_even
added theorem Stream'.get_inits
added theorem Stream'.get_map
added theorem Stream'.get_nats
added theorem Stream'.get_odd
added theorem Stream'.get_of_bisim
added theorem Stream'.get_succ
added theorem Stream'.get_succ_cons
added theorem Stream'.get_tail
added theorem Stream'.get_tails
added theorem Stream'.get_zero_cons
added theorem Stream'.get_zip
modified theorem Stream'.head_drop
added theorem Stream'.mem_of_get_eq
deleted theorem Stream'.mem_of_nth_eq
deleted theorem Stream'.nth_const
deleted theorem Stream'.nth_drop
deleted theorem Stream'.nth_enum
deleted theorem Stream'.nth_even
deleted theorem Stream'.nth_inits
deleted theorem Stream'.nth_map
deleted theorem Stream'.nth_nats
deleted theorem Stream'.nth_odd
deleted theorem Stream'.nth_of_bisim
deleted theorem Stream'.nth_succ
deleted theorem Stream'.nth_succ_cons
deleted theorem Stream'.nth_succ_iterate'
deleted theorem Stream'.nth_succ_iterate
deleted theorem Stream'.nth_tail
deleted theorem Stream'.nth_tails
deleted theorem Stream'.nth_zero_cons
deleted theorem Stream'.nth_zero_iterate
deleted theorem Stream'.nth_zip
modified theorem Stream'.take_succ'