Theorem Function.Bijective.sum_map

Modification history

2025-02-20 18:07
Mathlib/Data/Sum/Basic.lean
chore: rename Injective.sum_elim and friends (#22129) …
Deleted Function.Bijective.sum_mapView on Github →
2023-03-12 17:43
Mathlib/Data/Sum/Basic.lean
feat: forward-port leanprover-community/mathlib#18446 (#2346)
Added Function.Bijective.sum_mapView on Github →