OfNat for `Units`?

Stream: mathlib4

[Yury G. Kudryashov]

I want to add an instance that will allow us to write (n : Rˣ) assuming [Invertible (n : R)]. Are there any objections?

[Jon Eugster]

One related construction would be the one here: docs#EqualCharZero.pnatCast

I had to write a bunch of auxilary stuff to be able to write a function x ↦ (x.num : R) /ₚ ↑x.pnatDen : ℚ → R, so maybe your new instance would help simplify that, so that one could simply write x ↦ (x.num : R) /ₚ ↑x.den : ℚ → R after proving that in the setting of this file we always have such an Invertible instance :thinking:

[Yury G. Kudryashov]

I was thinking about literals, not cast. Cast has to be a globally defined function.