## Stream: new members

### Topic: Type confusion

#### Gareth Ma (Feb 02 2023 at 14:46):

Hi. I am dealing with rationals numbers and integers at the same time (oh no), and I am getting very lost converting between all the types. This is what I have:

lemma nice_lemma {q : ℚ} {n : ℤ} (h : n ≠ 0) : (q * n).denom = 1 ↔ ↑q.denom ∣ n :=
begin
replace hn : (n : ℚ) ≠ 0, by rwa [ne.def, ← int.cast_zero, rat.coe_int_inj],
split; intros h,
{ rw [← rat.num_div_denom q, div_eq_mul_inv, mul_assoc, mul_comm _ ↑n, ← mul_assoc,
← div_eq_mul_inv, ← int.cast_mul, show (q.denom : ℚ) = ↑(q.denom : ℤ), by exact rfl,
rat.denom_div_cast_eq_one_iff] at h,
{ exact int.dvd_of_dvd_mul_right_of_gcd_one h (coprime.symm q.cop), },
{ norm_cast, exact rat.denom_ne_zero q, }, },
{ rw [← rat.num_div_denom q, div_eq_mul_inv, mul_assoc, mul_comm _ ↑n, ← mul_assoc,
← div_eq_mul_inv, ← int.cast_mul, show (q.denom : ℚ) = ↑(q.denom : ℤ), by exact rfl,
rat.denom_div_cast_eq_one_iff],
{ apply dvd_mul_of_dvd_right h, },
{ norm_cast, exact rat.denom_ne_zero q, }, },
end

lemma nice_lemma' {q : ℚ} {n : ℕ} (h : n ≠ 0) : (q * n).denom = 1 ↔ q.denom ∣ n :=
begin

end


I have two questions:

1. It is clear that the proof of nice_lemma has a block of literal copy and paste, but I cannot seem to get rid of it. I tried rw before split but it only rw once, and I will have to rw twice to get the effect I want. Using simp only runs into self-modifying (?) issues. Can someone provide a better solution, or even an existing lemma that will do the work? I looked for a while but can't find anything.
2. How to prove nice_lemma' from nice_lemma? I want to do something like lift n to \Z, but it failed and I don't know what I am doing.

#### Riccardo Brasca (Feb 02 2023 at 14:52):

You need an intermediate lemma saying that if (q : ℚ) and (n : ℕ) then (n : ℤ) * q = n * q. This shouldn't be hard (maybe it is rfl). Then you have to convert the assumption n ≠ 0 to (n : ℤ) ≠ 0, and this is surely in the library.

#### Gareth Ma (Feb 02 2023 at 15:07):

Thank you! After doing all that then golfing and collapsing everything, I got this :)

lemma nice_lemma' {q : ℚ} {n : ℕ} (h : n ≠ 0) : (q * n).denom = 1 ↔ q.denom ∣ n :=
by exact iff.trans (nice_lemma (cast_ne_zero.2 h)) int.coe_nat_dvd


One line!

#### Patrick Massot (Feb 02 2023 at 15:13):

That line is too long, it should be (nice_lemma (cast_ne_zero.2 h)).trans int.coe_nat_dvd

#### Patrick Massot (Feb 02 2023 at 15:13):

(without by exact which is useless)

#### Eric Wieser (Feb 02 2023 at 15:14):

by exact_mod_cast (@nice_lemma _ n \$ by exact_mod_cast h) also works

#### Gareth Ma (Feb 02 2023 at 15:15):

Oh wow, let me understand them slowly :) Sooo much to learn

#### Gareth Ma (Feb 02 2023 at 15:35):

What is the @ doing? I don't understand the error after removing it.

#### Pedro Sánchez Terraf (Feb 02 2023 at 16:00):

Gareth Ma said:

What is the @ doing? I don't understand the error after removing it.

It makes all arguments explicit (in this case, q and n).

Last updated: Dec 20 2023 at 11:08 UTC