Zulip Chat Archive

Stream: Is there code for X?

Topic: gcd_nsmul_eq_zero?


view this post on Zulip Julian Külshammer (Mar 22 2021 at 20:11):

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?

view this post on Zulip Yakov Pechersky (Mar 22 2021 at 20:18):

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

view this post on Zulip Yakov Pechersky (Mar 22 2021 at 20:18):

And no defeq abuse =)

view this post on Zulip Julian Külshammer (Mar 23 2021 at 08:20):

Thanks. I added it to #6770.


Last updated: May 17 2021 at 16:26 UTC