Commit 2024-09-20 01:19 85cefec2
View on Github →chore(Data/Finset): change nonempty_cons to cons_nonempty (#16952)
In analogy with insert_nonempty (and other Finset nonempty lemmata), this should be named cons_nonempty rather than nonempty_cons.