Commit 2024-07-03 11:27 c4d01264
View on Github →chore: move iterate_prod_map to Data.Prod.Basic (#14367)
The lemma Function.iterate_prod_map is too fundamental to belong to a Dynamics folder.
It is moved to Data.Prod.Basic. The name of the lemma is changed from iterate_prod_map to Prod.map_iterate, which is more coherent with the usual naming (see Continuous.iterate, pow_iterate...) and thus more searchable.