gcd_nsmul_eq_zero?

Stream: Is there code for X?

[Julian Külshammer]

In data.int.gcd there is the following lemma:

lemma pow_gcd_eq_one {M : Type*} [monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) :
  x ^ m.gcd n = 1 := sorry

I'm looking for the additive version of this, i.e. something like this:

lemma gcd_nsmul_eq_zero {A : Type*} [add_monoid A] (x : A) {m n : ℕ} (hm : m •ℕ x = 0) (hn : n •ℕ x = 0) :
  (m.gcd n) •ℕ x = 0 := sorry

Is this somewhere in mathlib?

[Yakov Pechersky]

lemma nsmul_gcd_eq_zero {M : Type*} [add_monoid M] (x : M) {m n : ℕ} (hm : m •ℕ x = 0) (hn : n •ℕ x = 0) :
  (m.gcd n) •ℕ x = 0 :=
begin
  apply multiplicative.of_add.injective,
  rw [of_add_nsmul, of_add_zero, pow_gcd_eq_one];
  rwa [←of_add_nsmul, ←of_add_zero, equiv.apply_eq_iff_eq]
end

[Yakov Pechersky]

And no defeq abuse =)

[Julian Külshammer]

Thanks. I added it to #6770.