basic): improve docstring of `equiv.sum_equiv_sigma_bool` (#5119)

Commit

5 years ago

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`.

Author

urkud

Parents

d3cc9935

mathlib3 cb9e5cf9 - doc(data/equiv/basic): improve docstring of `equiv.sum_equiv_sigma_bool` (#5119)

mathlib3
cb9e5cf9 - doc(data/equiv/basic): improve docstring of `equiv.sum_equiv_sigma_bool` (#5119)