Element of \Q^x

Stream: new members

[Gareth Ma]

How should I construct an element of $\mathbb{Q}^{\times}$?

def a : ℚˣ := 2

I can do it explicitly with \<2, 1 / 2, by trivial, by trivial\>, but I was wondering if there's a simpler way, especially since $\mathbb{Q}$ is a field

[Eric Wieser]

I think there's a docs#Units.mk0

[Julian Berman]

That seems to work -- is there a plan to make those h \ne 0 goals default to by positivity eventually so you only need to write def a : ℚˣ := .mk0 2?

[Gareth Ma]

Thanks

[Eric Wieser]

I think in this case we could consider an ofNat instance

[Yaël Dillies]

We can't make those side goals default to positivity (at least naively) because positivity requires a bunch more imports.