Naming consistency wishlist

[BoltonBailey]

This is a tracking issue for several naming inconsistencies I have found. Feel free to add items to it.

• Polynomial.monomial_mul_monomial is analogous to MvPolynomial.monomial_mul?
• Finset.pred_card_le_card_erase: Why does this use - 1 instead of pred when pred rather than sub_one is in the name?
  • Seems that either
    • The name of this lemma should be changed
    • The lemma should be changed to use pred
• We have Finset.sum_add_distrib, but we also have a number of lemmas named more like sum_add.
• Closure operations refer to base relation constructor differently
  • EqvGen uses rel for the base relation constructor
  • Relation.ReflGen uses single for the base relation constructor
  • Relation.TransGen uses single too
  • conGen uses of for the base relation constructor.
• OrderedSub has a field with the substring tsub but as far as I can tell, this subtraction is not necessarily truncated.

[grunweg]

prod_map vs prodMap: see past zulip discussions