mathlib
efb4e959 - refactor(*iterate*): move to `function`; renamings (#2832)

Commit
6 years ago
refactor(*iterate*): move to `function`; renamings (#2832) * move lemmas about `iterate` from `data.nat.basic` to `logic.function.iterate`; * move lemmas like `nat.iterate_succ` to `function` namespace; * rename some lemmas: - `iterate₀` to `iterate_fixed`, - `iterate₁` to `semiconj.iterate_right`, see also `commute.iterate_left` and `commute.iterate_right`; - `iterate₂` to `semiconj₂.iterate`; - `iterate_cancel` to `left_inverse.iterate` and `right_inverse.iterate`; * move lemmas `*_hom.iterate_map_*` to `algebra/iterate_hom`.
Author
Parents
Loading