Zulip Chat Archive

Stream: general

Topic: rat.denom_div_cast_eq_one_iff


view this post on Zulip Johan Commelin (Jun 01 2020 at 08:11):

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

view this post on Zulip Johan Commelin (Jun 01 2020 at 10:05):

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...

view this post on Zulip Johan Commelin (Jun 01 2020 at 10:06):

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


Last updated: May 06 2021 at 21:09 UTC