lcm {1,...,n}

Stream: general

[Julian Külshammer]

As a small side project, I'm trying to determine the exponent of the symmetric groups, which is the lcm of the first n positive integers. I wanted to start by writing this as a product of prime powers. So far, I haven't even figured out how to formulate the statement. The following is my current attempt after some iterations. I understand that Lean complains that I am giving it a set where it wants a finset. How can I change this? Are there other comments regarding my current attempt?

import data.list.range
import ring_theory.int.basic
import algebra.big_operators
import data.nat.log
import algebra.gcd_monoid.multiset


open_locale big_operators

lemma lcm_iota {n : ℕ} :  multiset.lcm (coe (list.iota n)) = ∏ p in {p : ℕ | p.prime ∧ p ≤ n}, p ^ (nat.log p n) :=
begin
  sorry
end

[Yaël Dillies]

You may want docs#multiset.Icc?

[Yaël Dillies]

And for the RHS you can write it as (finset.Iic n).filter prime

[Julian Külshammer]

I get that it is missing decidable_pred prime. Do I need an additional import for that?

[Julian Külshammer]

Otherwise, open_locale classical also seems to work.

[Yaël Dillies]

docs#nat.decidable_prime should do its job.

[Yaël Dillies]

It's weirdly not stated as decidable_pred, but that shouldn't matter.

[Julian Külshammer]

Thanks. Unfortunately, I don't quite understand how to enable this def in my file?

[Yaël Dillies]

Isn't import data.nat.prime enough?

[Yakov Pechersky]

There are two decidability definitions of nat.prime, each of which has different pros and cons, kernel vs VM