Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-20 11:25 c781c0ea

View on Github →

feat(data/prod/basic): Involutivity of prod.map (#14845) If f and g are involutive, then so is prod.map f g.

Estimated changes

Modified src/data/prod/basic.lean

added theorem function.bijective.prod_map

modified theorem function.injective.prod_map

added theorem function.involutive.prod_map

added theorem function.left_inverse.prod_map

added theorem function.right_inverse.prod_map

modified theorem function.surjective.prod_map