Commit 2022-12-05 23:25 f7a138da

feat: port algebra.divisibility.basic (#833) Based off mathlib3 SHA: 70d50ecfd4900dd6d328da39ab7ebd516abe4025 There were a few changes in behavior from Lean 3 to Lean 4:

• Exists.intro c h -> Exists.intro c h.symm in the proof of Dvd.intro (h : a * c = b no longer unifies with b = a * c?)
• dvd_refl -> fun {a} => dvd_refl a in the proof of dvd_rfl (a | a no longer unifies with ∀ {a : α}, a ∣ a?)