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.