Commit 2020-08-23 05:18 ff970553
View on Github →feat(data/finset/basic): insert_singleton_comm (#3914)
Add the result that ({a, b} : finset α) = {b, a}. This came up in
#3872, and library_search does not show it as already present.
feat(data/finset/basic): insert_singleton_comm (#3914)
Add the result that ({a, b} : finset α) = {b, a}. This came up in
#3872, and library_search does not show it as already present.