multiplication by a unit is injective

Stream: Is there code for X?

[Michael Stoll]

I can't find the following in the library:

import tactic.apply_fun
import algebra.group_with_zero.basic

example {M} [monoid_with_zero M] {m : M} (hm : is_unit m) : function.injective (λ x, m * x) :=
begin
  intros x y h,
  simp only at h,
  cases hm with u hu,
  rw ← hu at h,
  let ui := u⁻¹,
  apply_fun (λ z : M, ↑ui * z) at h,
  simp only [units.inv_mul_cancel_left] at h,
  exact h,
end

There is mul_left_injective₀, but it requires a cancel_monoid_with_zero (and then works for all non-zero elements) and group_with_zero.mul_left_injective, which (as the name indicates) even needs a group_with_zero.

[Michael Stoll]

Found a shorter proof:

import tactic.apply_fun
import algebra.group_with_zero.basic
import algebra.regular.basic

example {M} [monoid_with_zero M] {m : M} (hm : is_unit m) : function.injective (λ x, m * x) := (is_unit.is_regular hm).left

[Michael Stoll]

So maybe it's not worth the effort of adding?

[Thomas Browning]

There is also

example {M} [monoid_with_zero M] {m : M} (hm : is_unit m) : function.injective (λ x, m * x) :=
λ _ _, (hm.mul_right_inj).mp

[Yaël Dillies]

I'm adding it in #14212 already

[Michael Stoll]

Thomas Browning said:

There is also

example {M} [monoid_with_zero M] {m : M} (hm : is_unit m) : function.injective (λ x, m * x) :=
λ _ _, (hm.mul_right_inj).mp

Ah, OK. There are too many places where to look... (and I was looking for injective and not just inj).

[Kevin Buzzard]

I think it's got to the point now where nobody knows all the library; after a while you either know where it is, or how to find it, or who to ask :-)

[Violeta Hernández]

I call dibs on the entire set_theory folder :P

[Yaël Dillies]

And me order :sweat_smile: