Commit 2022-09-01 09:13 8d90fcdb

View on Github →

feat(data/finset/basic): Add coe_pair lemmas (#16235) Adds coe_pair lemmas to go with coe_singleton and coe_eq_singleton (and fixes a couple of style issues).

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.coe_eq_pair

modified theorem finset.coe_eq_singleton

added theorem finset.coe_pair

modified theorem finset.cons_eq_insert

modified theorem finset.pair_comm