## Stream: new members

### Topic: rat.denom_zero

#### Lars Ericson (Jan 14 2021 at 02:00):

There is a rat.denom_one. There is no rat.denom_zero. However, given the goal

⊢ 0.denom = 1


the tactic

exact rfl,


will close the goal.

Question: What is happening under the hood with exact rfl?

#### Thomas Browning (Jan 14 2021 at 02:00):

rfl means that things are definitionally equal

#### Thomas Browning (Jan 14 2021 at 02:00):

refl should also work

#### Thomas Browning (Jan 14 2021 at 02:05):

Here's why 0.denom = 1 is definitionally equal.

First, 0 is defined as: instance : has_zero ℚ := ⟨of_int 0⟩
Second, of_int is defined as def of_int (n : ℤ) : ℚ := ⟨n, 1, nat.one_pos, nat.coprime_one_right _⟩
These four arguments correspond to the four arguments in the definition of a rational:

structure rat := mk' ::
(num : ℤ)
(denom : ℕ)
(pos : 0 < denom)
(cop : num.nat_abs.coprime denom)


Thus, of_int n means the rational number with num = n, denom = 1. In particular, (of_int n).num = n by definition and (of_int n).denom = 1 by definition.

#### Thomas Browning (Jan 14 2021 at 02:05):

(This is all coming from data/rat/basic.lean)

#### Thomas Browning (Jan 14 2021 at 02:09):

So both of these examples are definitionally true (and 0.denom = 1 is a special case of the second example).

example (n : ℤ) : (rat.of_int n).num = n := rfl
example (n : ℤ) : (rat.of_int n).denom = 1 := rfl


Thank you!

#### Eric Wieser (Jan 14 2021 at 08:40):

Presumably denom_zero should be added as a simp lemma?

Last updated: May 16 2021 at 05:21 UTC