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.

Estimated changes