rat.denom_div_cast_eq_one_iff

Stream: general

[Johan Commelin]

What should this be called? Is this the optimal form?

lemma rat.denom_div_cast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) :
  ((m : ℚ) / n).denom = 1 ↔ n ∣ m :=
begin
  split,
  { intro h,
    lift ((m : ℚ) / n) to ℤ using h with k hk,
    use k,
    rw eq_div_iff_mul_eq _ _ (show (n:ℚ) ≠ 0, by exact_mod_cast hn) at hk,
    norm_cast at hk,
    rw [← hk, mul_comm], },
  { rintros ⟨d, rfl⟩,
    rw [int.cast_mul, mul_comm, mul_div_cancel, rat.coe_int_denom],
    exact_mod_cast hn }
end

[Johan Commelin]

maybe a nicer way of stating this is to use is_integral from integral closures etc... but that would pull half of the algebra library in as a dependency...

[Johan Commelin]

Also can_lift int nat uses r.denom = 1 as hypothesis