Showing that ↑a / ↑b = ↑(a / b)

Stream: maths

[Sebastian Zimmer]

I have to rational numbers a, b and I need to show that that casting to Real respects division.
i.e. (a : ℝ) / (b : ℝ) = ((a / b : ℚ) : ℝ)

I would have thought that either simp or norm_cast would help but apparently not. How should I show this, and also how can I search for relevant theorems? rw? didn't seem to come up with anything useful.

[Aaron Liu]

I also think either simp or norm_cast should work but if they don't you can always just use docs#Rat.cast_div directly.

[Sebastian Zimmer]

Ah I was missing an import import Mathlib.Data.Rat.Cast.CharZero.

What would have been the easiest way for me to find this without asking here?

[Aaron Liu]

import Mathlib and only reduce your imports once you're done writing all the code (that's what I do).

[Aaron Liu]

Of course, if you're working on mathlib, this doesn't quite work.

[Kevin Buzzard]

If you're working within an already-existing file then almost always you either have enough stuff imported already, or you know what more you need to import already. If you're working on a new file then you start with import Mathlib and minimise later. This is my experience, but then again it might not be representative of everyone because I tend to work very far from the root.