Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-16 16:42 f4ecb599

View on Github →

feat(data/sum/basic): add some missing lemmas (#18184) Forward-ported to Mathlib 4 in leanprover-community/mathlib4#1583

Estimated changes

added theorem sum.elim_map
modified theorem sum.get_left_eq_none_iff
modified theorem sum.get_right_eq_none_iff