Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-17 21:55 27a777b1

View on Github →

feat(data/nat/gcd): coprime.lcm_eq_mul (#9761) Surprisingly, this result doesn't seem to be present yet.

Estimated changes

modified theorem nat.coprime.gcd_eq_one
added theorem nat.coprime.lcm_eq_mul