d | a -> d | (a * b)?

Stream: maths

[Kevin Buzzard]

Having just spent ten minutes looking for dvd_left or whatever it's called I'm finally giving up and asking here. Sorry. Everything is a nat. I can prove it -- I just want it to be there already.

[Kevin Buzzard]

dvd_mul_of_dvd_left. I was looking in nat. It's in core lean in algebra/ring.