Commit 2023-10-19 20:25 267b8cb1
View on Github →feat: natDegree_sub_C (#7776)
Adds degree_sub_C, natDegree_sub_C, analogous to ..._add_C.
Also relocates C_neg and C_sub to Basic.lean (where C_add is) so that the new lemmas can be in the same file as their add counterparts.