Commit 2024-06-24 19:38 f584eb98
View on Github →feat(Data/Prod): add map_comp_swap (#14096)
This PR adds theorem Prod. map_comp_swap stating that for two functions f and g of type α → α, the composition of Prod.map f g with Prod.swap is equal to the composition of Prod.swap with Prod.map g f.