Casting LCM

Stream: Is there code for X?

[Gareth Ma]

Hi, is there a lemma for ↑(s.lcm (coe : ℕ → ℕ)) = s.lcm (coe : ℕ → ℝ)?

[Gareth Ma]

I also tried proving from scratch by induction, but then I run into another goal:

example {s : finset ℕ} : ↑(s.lcm (coe : ℕ → ℕ)) = s.lcm (coe : ℕ → ℝ) :=
begin
  simp_rw [finset.lcm],
  apply finset.induction_on s,
  simp,
  intros a s ha h,
  simp_rw [fold_insert ha, ← h],
  rw nat.cast_id,
end
-- h: ↑(fold lcm 1 coe s) = fold lcm 1 coe s
-- ⊢ ↑(lcm a (fold lcm 1 coe s)) = lcm ↑a ↑(fold lcm 1 coe s)

[Jireh Loreaux]

I don't think the finset.lcm in ℝ is what you think it is. In particular, I'm pretty sure it only takes the values 0 or 1, depending on whether 0 is in the finset or not.

[Jireh Loreaux]

In particular, the normalized_gcd_monoid instance on ℝ comes from docs#comm_group_with_zero.normalized_gcd_monoid, and the definition of lcm there is: lcm := λ (a b : G₀), ite (a = 0 ∨ b = 0) 0 1.

[Jireh Loreaux]

Then finset.lcm is just a fold over this.

[Gareth Ma]

Ohh hmm, that's clearly not what I want :joy: Let me take a look at what I need again. Thanks!

[Jireh Loreaux]

On another note: coe : nat -> nat is weird. Why try to coerce from nat to itself? Maybe you want id there?

[Gareth Ma]

Yea, my original version had id, but I thought that if such a theorem exists, it might be in the form of .lcm_coe_coe or something instead of lcm_id_coe haha.