multiplicity_gcd

Stream: Is there code for X?

[Xavier Xarles]

I have a proof for the result (and analogous for lcm and max),

import data.nat.gcd

lemma multiplicity_gcd {p m n : ℕ} (hp : p.prime):
  multiplicity p (nat.gcd m n) = min (multiplicity p m) (multiplicity p n) :=sorry

I think is not in mathlib. I did it to practice and because I need it for a project.

[Ruben Van de Velde]

Seems worth adding

[Kevin Buzzard]

@Xavier Xarles are you saying you have a proof? Please feel free to add it if it's not there!

[Xavier Xarles]

Kevin Buzzard said:

Xavier Xarles are you saying you have a proof? Please feel free to add it if it's not there!

I am not sure how to do it. I will talk with Marc Masdeu and ask him... On the other hand, I will ask also to help me to put in a more mathlib form...

[Bhavik Mehta]

I have this lemma in some file for the unit fractions project, I agree its useful

[Xavier Xarles]

I would like to make a PR on that. My GitHub is @XavierXarles.

[Riccardo Brasca]

I've sent you an invitation

[Stuart Presnell]

Is this the same as docs#factorization_gcd?

lemma factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :
  (gcd a b).factorization = a.factorization ⊓ b.factorization

[Stuart Presnell]

But we don't have the corresponding lemma for lcm and ⊔.