zmod n to ℚ

Stream: maths

[Ashvni Narayanan]

I don't understand why this is true :
example (n : ℕ) (a b : zmod n) : ((a * b) : ℚ) = (a : ℚ) * (b : ℚ) :=
The proof is refl. As far as I understand, the coercion to ℚ arises from the map to ℕ taking a : zmod n to a.val, which is not multiplicative..
Any help is appreciated, thank you!

[Kevin Buzzard]

The proof is refl because elaboration works from the outside in. Lean sees (a * b : ℚ) and its first thought is _not_ "oh, a and b are in zmod n, so that * must be multiplication in zmod n", it says "Oh OK, so the result of this multiplication is supposed to be in ℚ so that multiplication must definitely be rat.mul -- now let's elaborate further; oh look, a and b are in zmod n, we wanted things in rat so let's coerce." The result is that the two sides of the equality in your example are the same.

[Ashvni Narayanan]

I see, thank you!

[Patrick Massot]

Let me elaborate a bit since this is an important and tricky topic. First thing to notice is that the goal clearly shows the coercion arrows are not where you want them to be. Then you need to understand when Lean insert coercion arrows.

[Kevin Buzzard]

Oh yeah as Patrick says, if you look at your goal for the refl goal it's ⊢ ↑a * ↑b = ↑a * ↑b. The way to make the false goal is

example (n : ℕ) (a b : zmod n) : ((a * b : zmod n) : ℚ) = (a : ℚ) * (b : ℚ) := rfl -- fails

which gives you a goal ⊢ ↑(a * b) = ↑a * ↑b

[Patrick Massot]

Basically Lean works left to right, soliving constraints as soon as possible and inserts a coercion only when desperate. Here you need to remember that the infix notation is only a notation, so ((a * b) : ℚ) is really a has_mul.mul a b : ℚ. Given the type ascription, Lean knows the multiplication has to be multiplication of rational numbers. Then it moves to a. This is not a rational and there is nothing else to try so Lean inserts a coercion. Then the same happen with b.

[Ashvni Narayanan]

Oh I see, thank you!