lcm_pos_pos

Stream: Is there code for X?

[Xavier Xarles]

Do we have the following?

theorem lcm_pos_pos {m n : ℕ} (hm : 0<m ) (hn : 0<n ) : 0<lcm m n :=
begin
  have hmn:=mul_pos hm hn,
  rw ←(nat.gcd_mul_lcm m n) at hmn,
  have hg: 0≤gcd m n:=dec_trivial,
  exact pos_of_mul_pos_left hmn hg,
end

[Riccardo Brasca]

We have docs#nat.lcm_ne_zero that is essentially what you want.

[Riccardo Brasca]

So

theorem lcm_pos_pos {m n : ℕ} (hm : 0<m ) (hn : 0<n ) : 0 < lcm m n :=
nat.pos_of_ne_zero $ nat.lcm_ne_zero hm.ne' hn.ne'

should work (untested).