|
|
|
|
|
|
by jhanschoo
315 days ago
|
|
|
A lemma like this is common for well-known results https://github.com/leanprover-community/mathlib4/blob/fc728c... The one immediately before (`gcd_mul_dvd_mul_gcd`) is also well-known but uses a style closer to forward proof. The very well-known ones `gcd_assoc` at the start oof this file are even more extreme and directly supply the proof term without tactics. |
|
|