Commit 2023-03-12 17:43 f5505623

View on Github →

feat: forward-port leanprover-community/mathlib#18446 (#2346)

Estimated changes

Modified Mathlib/Data/Prod/Basic.lean

added theorem Prod.map_bijective

added theorem Prod.map_injective

added theorem Prod.map_involutive

added theorem Prod.map_leftInverse

added theorem Prod.map_rightInverse

added theorem Prod.map_surjective

Modified Mathlib/Data/Sum/Basic.lean

added theorem Function.Bijective.sum_map

added theorem Sum.map_bijective

added theorem Sum.map_injective

added theorem Sum.map_surjective