Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-15 23:35 45619c73

View on Github →

feat(order/iterate): id_le lemmas (#7943)

Estimated changes

Modified src/order/iterate.lean

added theorem function.commute.id_le_iterate_of_id_le

added theorem function.commute.iterate_le_id_of_le_id

added theorem function.commute.iterate_le_iterate_of_id_le

added theorem function.commute.iterate_le_iterate_of_le_id