## Stream: general

### Topic: rat.mk_eq

#### Kenny Lau (Apr 25 2018 at 14:55):

theorem mk_eq : ∀ {a b c d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0),
a /. b = c /. d ↔ a * d = c * b :=
suffices ∀ a b c d hb hd, mk_pnat a ⟨b, hb⟩ = mk_pnat c ⟨d, hd⟩ ↔ a * d = c * b,
[...]


#### Kenny Lau (Apr 25 2018 at 14:56):

the one in suffices is what I need T_T

#### Mario Carneiro (Apr 25 2018 at 17:03):

Just rewrite mk_pnat into /., they are equal

#### Kenny Lau (Apr 25 2018 at 17:04):

this is what I did at the end:

theorem rat.mk_pnat_eq_iff (a b c d) : rat.mk_pnat a b = rat.mk_pnat c d ↔ a * d = c * b :=
begin
cases b with b hb, cases d with d hd,
simp [rat.mk_pnat_eq],
rw [rat.mk_eq],
exact ne_of_gt (int.coe_nat_pos.2 hb),
exact ne_of_gt (int.coe_nat_pos.2 hd),
end


#### Kenny Lau (Apr 25 2018 at 17:04):

this part of the code is not going to be PR'd so the neatness of the proof doesn't really matter ot me

#### Kenny Lau (Apr 25 2018 at 17:04):

but I did write a whole bunch of lemmas in the meantime

#### Mario Carneiro (Apr 25 2018 at 17:07):

The real question is why are you dealing with mk_pnat? The interface should let you just use field operations and avoid mk entirely

#### Kenny Lau (Apr 25 2018 at 17:08):

oh, mk_pnat is not intended to be used?

#### Kenny Lau (Apr 25 2018 at 17:08):

I used it because I am using pnat

#### Kenny Lau (Apr 25 2018 at 17:08):

or are you going to tell me that pnat is not to be used either

#### Mario Carneiro (Apr 25 2018 at 17:10):

Just use n / d where d : N+

#### Mario Carneiro (Apr 25 2018 at 17:11):

The only reason you might want mk_pnat is if you care about the efficiency of computing this value (this will translate d to rat by adding ones)

Last updated: May 13 2021 at 06:15 UTC