mul_lt_mul''''

Stream: general

[Patrick Massot]

Amazing, @Scott Morrison got rid of the name mul_lt_mul'''' just when I was feeling bad PRing code using it! :heart:

[Scott Morrison]

The background here is that mathport was having trouble with multiple primes (it sometimes needs to add primes itself, and we were getting name collisions because it couldn't anticipate not-yet-imported files also adding primes). That can be (has been?) fixed by adding _' instead, but in any case primes in names are pretty lame. :-)

I would be happy if we limited ourselves to a single prime, and otherwise put more effort into thinking up names. :-) Even with a single prime, anytime we can articulate a class of reasons for adding a prime, we should think of a naming scheme that can reflect that reason.

I was worried people would be annoyed at minor renaming like this, so I'm glad Patrick celebrated the demise of mul_lt_mul''''. :-)

[Floris van Doorn]

The lemmas related to docs#has_ordered_sub are a big source of primes, since they are usually variant of lemmas about add_group.
One possibility is to use the naming convention that a subtraction with a has_ordered_sub instance is called tsub instead of sub (short for "truncated subtraction"). This is very similar to the distinction between Inf and cInf.
Is that a good idea?

[Yaël Dillies]

Note that you'll also get to rename data.nat.psub. Sorry, got confused.

[Floris van Doorn]

Ok, there seems to be support for using tsub, so I'll do that after the other ordered sub PRs I am doing/planning now.

Note: I'm planning to rename the lemmas for a variable type that use tsub, but not for specific types. So we will have tsub_le_tsub_add_tsub and ennreal.lt_add_of_sub_lt. Does that sounds reasonable? I think that is consistent with calling infimum on ℝ Inf and not cInf.

[Yaël Dillies]

No strong opinion, but I kind of wanted to rename the Inf on ℝ to cInf.

[Kevin Buzzard]

I guess it's not actually an Inf so I can definitely get behind this idea