mul_left_inj and mul_right_cancel_iff

Stream: mathlib4

[Jeremy Parker]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#mul_left_inj
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#mul_right_cancel_iff
Why are there these two near-identical results? Is this a historical quirk? Should one be deprecated? Or am I missing some subtlety about the two slightly different statements?

I opened #30468 to create a version of the latter for GroupWithZero, but it was pointed out that GroupWithZero already has a version of the former.

[Kenny Lau]

wow, even in the same file and very close to each other

[Kenny Lau]

image.png

[Kenny Lau]

it seems like they were originally in different files

[Anne Baanen]

It goes even further: mathlib3#2707 suggests they were originally in core Lean vs Mathlib.

[Anne Baanen]

mul_left_cancel_iff was defined in core Lean back in 2017-03-08: https://github.com/leanprover-community/lean/commit/4c88e2c5b0ff162fc3d96524e3142668b92a3795

mul_right_inj was defined in Mathlib back in 2017-09-16: https://github.com/leanprover-community/mathlib3/commit/a1c3e2defc89c1bc792cb34caf9947dd77aabd3f

And I suppose they have never really been merged ever since.

[Anne Baanen]

docs#mul_right_inj seems to be an order of magnitude more popular in Mathlib, shall we keep that one?

$ rg '\bmul_(left|right)_cancel_iff\b' | wc -l
      25
$ rg '\bmul_(left|right)_inj\b' | wc -l
     231

[Anne Baanen]

(Note that core Lean also has docs#Nat.mul_left_inj vs docs#Nat.mul_right_cancel_iff for even more confusion!)

[Aaron Liu]

again I'm confused why even though it's the same statement one is left and one is right

[Aaron Liu]

which one is correct (or are they both correct)?

[Jeremy Parker]

One is saying that left multiplying a by an element is injective. The other is saying that right multiplying by an element called a cancels. They're conceptually different but the statements are identical

[Kevin Buzzard]

Not quite identical -- one assumes a ≠ 0 and the other assumes 0 < a ;-)

[Aaron Liu]

Jeremy Parker said:

One is saying that left multiplying a by an element is injective. The other is saying that right multiplying by an element called a cancels. They're conceptually different but the statements are identical

Wait, no actually that's conceptually the same

[Aaron Liu]

I guess the difference is whether you view it as left multiplication or right multiplication

[Aaron Liu]

so which one is it

[Kevin Buzzard]

Anne Baanen said:

docs#mul_right_inj seems to be an order of magnitude more popular in Mathlib

That's because that's the one that exact? finds ;-)

import Mathlib

--#check mul_left_cancel_iff

example {G : Type*} [inst : Mul G] [IsLeftCancelMul G] {a b c : G} : a * b = a * c ↔ b = c := by
  exact?

[Matt Diamond]

recently I found docs#Option.mem_some and docs#Option.mem_some_iff which are not only identical but are defined one after the other

[Matt Diamond]

I'm wondering if this was on purpose though, as one is marked as a grind theorem and the second is defined as the first

[Matt Diamond]

is there some benefit to having grind-tagged and non-grind-tagged versions of a theorem?

[Matt Diamond]

actually it looks like it was added before the grind notation in this commit

weird... I can understand if we wanted to standardize on _iff suffixes or something like that, but if so, why not deprecate the previous version?

[Kim Morrison]

These are all just signs that is is difficult to maintain very large libraries! If it is obvious which name/variant is preferred, please open PRs! If it is not obvious, discuss here.

Can someone write a tool that detects exact duplicates up to naming? Up to reordering hypotheses? Up to common hypothesis variants (e.g. n \ne 0 and 0 < n in Nat)? etc? :-)

[Jovan Gerbscheid]

I wrote something like that in #mathlib4 > duplicate declarations

[Kevin Buzzard]

Ha oh yeah and the results were spectacular IIRC! (over 300 dupes I think?)

Link to text file is in this message #mathlib4 > duplicate declarations @ 💬

[Kevin Buzzard]

So the correct question is now whether someone can now write a tool which deprecates the right one of each dupe!