prod_Nat.dvd_and_dvd_of_dvd_prod

Stream: std4

[Scott Morrison]

Was

def prod_Nat.dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) :
    {d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1.val * d.2.val} :=

in https://github.com/leanprover/std4/pull/169/files intentional? Seems a strange name!

[Patrick Massot]

Oops, this is clearly a search and replace accident. I'm sorry, I'll fix it later today.

[Patrick Massot]

I opened https://github.com/leanprover/std4/pull/170 with a fix. I apologize again.