Commit 2023-01-25 12:38 895e78b7

View on Github →

Feat: add lemmas about Sum (#1583) This is the Lean 4 version of leanprover-community/mathlib#18184

Estimated changes

Modified Mathlib/Data/Sum/Basic.lean

added theorem Sum.elim_map

modified theorem Sum.getLeft_eq_none_iff

added theorem Sum.getLeft_eq_some_iff

modified theorem Sum.getRight_eq_none_iff

added theorem Sum.getRight_eq_some_iff