Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-15 16:25 9451f8de

View on Github →

feat(data/sum): add sum.{get_left, get_right, is_left, is_right} (#3792)

Estimated changes

added def sum.get_left
added def sum.get_right
added def sum.is_left
added def sum.is_right