Topic: d | a -> d | (a * b)?
Kevin Buzzard (Aug 08 2018 at 16:34):
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 (Aug 08 2018 at 16:38):
dvd_mul_of_dvd_left. I was looking in
nat. It's in core lean in algebra/ring.
Last updated: May 18 2021 at 07:19 UTC