[Merged by Bors] - feat(algebra/invertible): add a missing lemma inv_of_eq_left_inv

[l534zhan]

add "inv_of_eq_left_inv"

---

[eric-wieser]

For other reviewers: is this version better or worse?

Suggested change

	lemma inv_of_eq_left_inv [monoid α] {a b : α} [invertible a] (hac : b * a = 1) : ⅟a = b :=
	(left_inv_eq_right_inv hac (mul_inv_of_self _)).symm
	lemma left_inv_eq_inv_of [monoid α] {a b : α} [invertible b] (hac : a * b = 1) : a = ⅟b :=
	left_inv_eq_right_inv hac (mul_inv_of_self _)

My thoughts were that it doesn't swap a and b, but that's perhaps not important.

[adomani]

Eric, I think that your version is better. I can get close to a proof of this: in my opinion, the eq_comm at the end of the code below, almost certifies that there two sides should not be swapped!

lemma inv_mul_injective [monoid α] (a : α) [invertible a] : function.injective ((*) a) :=
λ b c bc, by simpa using congr_arg ((*) (⅟ a)) bc

lemma mul_inv_injective [monoid α] (a : α) [invertible a] : function.injective (flip (*) a) :=
λ b c bc, have h : b * a * ⅟ a= c * a * ⅟ a := congr_arg (flip (*) (⅟ a)) bc,
by simpa [mul_assoc] using h

lemma invertible.mul_eq_mul_iff_left [monoid α] (a : α) {b c : α} [invertible a] :
  a * b = a * c ↔ b = c :=
⟨λ h, inv_mul_injective a h, congr_arg ((*) a)⟩

lemma invertible.mul_eq_mul_iff_right [monoid α] (a : α) {b c : α} [invertible a] :
  b * a = c * a ↔ b = c :=
⟨λ h, mul_inv_injective a h, congr_arg (flip (*) a)⟩

lemma inv_of_eq_left_inv [monoid α] {a b : α} [invertible a] : b * a = 1 ↔ ⅟a = b :=
by { rw [← invertible.mul_eq_mul_iff_right (⅟ a)], simp [eq_comm] }

[l534zhan]

I am following the format of the existing "inv_of_eq_right_inv"
lemma inv_of_eq_right_inv [monoid α] {a b : α} [invertible a] (hac : a * b = 1) : ⅟a = b := left_inv_eq_right_inv (inv_of_mul_self _) hac
Should we change them both together (which may produce further problems) or stick to the current format.

[jcommelin]

I think it's useful if the conclusion is of the form ⅟ foo = bar. That's the direction we will typically want to rw in. And for the rest, the statement should be the dual of inv_of_eq_right_inv. I don't have a strong opinion on whether or not to swap the a and the b in the statement.

[l534zhan]

Thanks, Johan. Then how about stick to my current format which is the dual of the existing one and approving the PR?
@jcommelin

[eric-wieser]

bors r+

I don't think it's worth spending any more time thinking about which version is best, since there's so little difference anyway. Let's just put in the version you suggested.

Thanks for the contribution!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests