Commit 2022-11-13 23:50 8e256c33

View on Github →

feat: port Logic.Function.Iterate (#585) For review purposes: Diff from mathport output TODO, in this PR or a later one: edit the proof of Iterate.rec to be computable. See Mario's comment.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Function/Iterate.lean

added theorem Function.Bijective.iterate

added theorem Function.Commute.comp_iterate

added theorem Function.Commute.iterate_eq_of_map_eq

added theorem Function.Commute.iterate_iterate

added theorem Function.Commute.iterate_iterate_self

added theorem Function.Commute.iterate_left

added theorem Function.Commute.iterate_right

added theorem Function.Commute.iterate_self

added theorem Function.Commute.self_iterate

added theorem Function.Injective.iterate

added def Function.Iterate.rec

added theorem Function.Iterate.rec_zero

added theorem Function.LeftInverse.iterate

added theorem Function.RightInverse.iterate

added theorem Function.Semiconj.iterate_left

added theorem Function.Semiconj.iterate_right

added theorem Function.Semiconj₂.iterate

added theorem Function.Surjective.iterate

added theorem Function.comp_iterate_pred_of_pos

added theorem Function.iterate_add

added theorem Function.iterate_add_apply

added theorem Function.iterate_comm

added theorem Function.iterate_commute

added theorem Function.iterate_fixed

added theorem Function.iterate_id

added theorem Function.iterate_mul

added theorem Function.iterate_one

added theorem Function.iterate_pred_comp_of_pos

added theorem Function.iterate_succ'

added theorem Function.iterate_succ

added theorem Function.iterate_succ_apply'

added theorem Function.iterate_succ_apply

added theorem Function.iterate_zero

added theorem Function.iterate_zero_apply

added theorem List.foldl_const

added theorem List.foldr_const