finset.lcm of positive integers is positive

Stream: Is there code for X?

[Julian Külshammer]

In #10249 I am defining the exponent of a group and some basic properties. I'm almost done proving the equivalence of the two definitions (via minimal n such that g^n=1 for all g and lcm of order). The only small sorry that is missing is that the lcm of a finset of positive integers is positive. Is this somewhere or at least something close enough? I'm also not sure what the right generality of such a result is apart from natural numbers.

[Eric Rodriguez]

docs#finset.lcm_eq_zero_iff? Not sure if this exists but the gcd one does

[Julian Külshammer]

It doesn't, but the link seems helpful. Thanks.