lcm equal first iff second divides first

Stream: Is there code for X?

[Xavier Xarles]

The following lemma is true (I have a proof in lean).

lemma lcm_eq_dvd (n m : nat): n.lcm m = m  ↔ n ∣ m:= sorry

[Damiano Testa]

This appears to work, but I do not know why:

import ring_theory.int.basic

lemma lcm_eq_dvd (n m : nat): n.lcm m = m ↔ n ∣ m:=
(lcm_eq_right_iff _ _ (normalize_eq _))

[Ruben Van de Velde]

What's confusing? nat only has a single unit

[Ruben Van de Velde]

Oh, and it also relies on nat.lcm being defeq to gcd_monoid.lcm, I guess

[Damiano Testa]

Actually, I was confused since I did not know what normalize meant, but then I looked it up.

[Yaël Dillies]

This is basically docs#sup_eq_right

[Ruben Van de Velde]

Oddly, trying to generalize away from nat, I'm stuck on normalized_gcd_monoid.to_normalization_monoid = normalization_monoid_of_unique_units

[Ruben Van de Velde]

Expecting someone to come up with a one-liner, but:

lemma lcm_eq_dvd {α : Type*} [cancel_comm_monoid_with_zero α] [gcd_monoid α] [unique αˣ] (n m : α) :
  lcm n m = m ↔ n ∣ m :=
begin
  letI : normalized_gcd_monoid α := {
    normalize_gcd := λ a b, normalize_eq _,
    normalize_lcm := λ a b, normalize_eq _,
    ..(by apply_instance : gcd_monoid α),
    ..normalization_monoid_of_unique_units },
  exact lcm_eq_right_iff n m (normalize_eq m),
end