basic): add some missing lemmas (#18184)

Commit

3 years ago

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

Author

urkud

Parents