lcm

Stream: general

[Dean Young]

What are some nice features of lean's lcm and gcd?

[Riccardo Brasca]

Can you be a little more precise with your question? In mathlib gcd and lcm are defined in great generality, so they can look a little strange if you're not familiar with these concepts in commutative algebra. On the other hand, for integres, they coincide with the usual notion.

[Dean Young]

I meant for the Int type.

[Yury G. Kudryashov]

"nice feature" is still too vague