Commit 2020-11-27 06:39 cb9e5cf9

View on Github →

doc(data/equiv/basic): improve docstring of equiv.sum_equiv_sigma_bool (#5119) Also slightly improve defeq of the to_fun field by using sum.elim instead of a custom match.

Estimated changes

Modified src/data/equiv/basic.lean

modified def equiv.sum_equiv_sigma_bool