IsUnit_of_isUnit_mul

Stream: Is there code for X?

[Andrew Yang]

Do we really not have this?

import Mathlib.Algebra.Group.Units.Defs
import Mathlib.Tactic.Common

lemma isUnit_of_isUnit_mul {M : Type*} [Monoid M] (x y : M)
    (h : Commute x y) (h' : IsUnit (x * y)) : IsUnit x := by
  obtain ⟨⟨_, ixy, h₁, h₂⟩, rfl⟩ := h'
  exact ⟨⟨_, y * ixy, by rwa [← mul_assoc],
    by simpa only [mul_one, ← h.eq, h₁, mul_assoc] using congr(y * $h₂ * x * ixy)⟩, rfl⟩

[Yury G. Kudryashov]

docs#Commute.isUnit_mul_iff

[Andrew Yang]

Oh thanks!
Not sure how exact? did not find it.

[Kim Morrison]

This lemma is an iff that produces IsUnit x ∧ IsUnit y. There's no way for apply to get to IsUnit x from that.

[Yury G. Kudryashov]

I found it using @loogle Commute, IsUnit (_ * _)
Also, it looks like I added it in 2021

[loogle]

:search: Commute.isUnit_mul_iff

[Kim Morrison]

If you add this (and the symmetric version) then exact? will find it next time.

[Yury G. Kudryashov]

It can be called, e.g., IsUnit.left_of_mul.

[Ruben Van de Velde]

Or Commute.isUnit_of_mul_left? (or should it be right, then)

[Yaël Dillies]

I think the Commute doesn't really need to be part of the name, or rather than primarily, so that the name can be similar to the CommMonoid lemma

[Andrew Yang]

There is already docs#isUnit_of_mul_isUnit_left which does not go through the non-commutative case, which was why I thought it didn't exist.
I'd prefer Commute.isUnit_of_mul_isUnit_left to mirror the commmonoid lemma.

[Yaël Dillies]

I would call the CommMonoid lemma IsUnit.left_of_mul and the Commute one IsUnit.left_of_mul_of_commute

[Ruben Van de Velde]

And rename docs#Commute.isUnit_mul_iff ?

[Yaël Dillies]

Don't really know about this one because no dot notation becomes available

[Yury G. Kudryashov]

I would leave Commute.isUnit_mul_iff as is, because it can be used with dot notation now.