Tracking Issue: Naming consistency

This is a tracking issue for naming inconsistencies. It is intended as a location for people to post naming inconsistencies they don't have bandwidth to fix, and for contributors or new users with free time to find ideas for making the naming system of Mathlib more coherent.

Other contributors should feel free to edit this comment to add items to it.

• Develop PR #11385 into something that will identify inconsistencies between different, but semantically similar, namespaces.

• 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.

• Monotonicity

  • We seem to have lemmas proving Monotone for various functions named with the forms monotone_foo and bar_monotone, seems like we could choose one form for consistency.

• The List.sum function is sometimes referred to in lemma names by list_sum and sometimes by listSum

• The contents of Algebra/BigOperators/Group/* mainly reference Monoids, rather than Groups. (see here #22145 and zulip #mathlib4 > long files @ 💬)

  1. The directory should be renamed Algebra/BigOperators/Monoid/*
  2. Lemmas that really are about groups should be then brought back to a new Algebra/BigOperators/Group/*

• tsum_geometric_nnreal seems like it should be named NNReal.tsum_geometric

• LinearEquiv.prod should be LinearEquiv.prodCongr instead: #24145 renames this

• Make the lower-case form of AEStronglyMeasurable consistent: #mathlib4 > Naming convention @ 💬; might need further discussion

• Should Prod.swap_prod_mk and friends be renamed to Prod.swap_prodMk? Still being discussed on zulip

• Both inv_two and two_inv appear in lemma names. We should make a consistent naming format for postfix functions like this.

• EReal.add_pos does not seem to have an analogue for Real (I guess this makes sense because of the generic add_pos, but this still feels odd to me somehow, see discussion below)

• Nat.digits_len - spelling out "length" seems to be the more normal way to reference List.length in a lemma name.

In general, this zulip thread may have further not-yet-resolved naming questions on them. (It may be necessary to gather consensus of those first.)

Start with the unchecked items in this tracking issue and inspect the linked definitions in Mathlib/Algebra/Polynomial/Basic.html, Mathlib/Data/Finset/Card.html, Mathlib/Logic/Relation.html, and the other referenced files. Review the linked Zulip discussions and related issues before choosing one item; done means consensus on a specific naming change and a focused change with the affected references updated.