Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-17 17:11 49bf1fde

View on Github →

chore(order/iterate): fix up the namespace (#7977)

Estimated changes

Modified src/order/iterate.lean

deleted theorem function.commute.id_le_iterate_of_id_le

deleted theorem function.commute.iterate_le_id_of_le_id

deleted theorem function.commute.iterate_le_iterate_of_id_le

deleted theorem function.commute.iterate_le_iterate_of_le_id

added theorem function.id_le_iterate_of_id_le

added theorem function.iterate_le_id_of_le_id

added theorem function.iterate_le_iterate_of_id_le

added theorem function.iterate_le_iterate_of_le_id