HPow

Stream: mathlib4

[Moritz Firsching]

I was looking at porting GroupTheory.CommutingProbability and there we define a rational number

/-- The commuting probability of a finite type with a multiplication operation -/
def commProb : ℚ :=
  Nat.card { p : M × M // p.1 * p.2 = p.2 * p.1 } / Nat.card M ^ 2
#align comm_prob commProb

But this fails with failed to synthesize instance HDiv ℚ ℕ ℚ. I'm trying to understand what is going on, and what is the correct way to fix this. It can be made to not complain anymore in many ways, for instance

Nat.card { p : M × M // p.1 * p.2 = p.2 * p.1 } / (HPow.hPow (Nat.card M) 2)

or

Nat.card { p : M × M // p.1 * p.2 = p.2 * p.1 } / (Nat.card M : ℚ) ^ (2)

and I'm unsure what to do.
When playing around with this I noticed there is already something about how heterogenous powers work.
Why does this work

-- works:
def qpow_example_1 : ℚ := 3^2
def qpow_example_2 : ℚ := (3 : ℕ) ^ (2 : ℕ)
def qpow_example_3 : ℚ := 3 ^ (2 : ℕ)
def qpow_example_4 : ℚ := HPow.hPow (3 : ℕ) 2

but this doesn't?

-- "failed to synthesize instance  HPow ℕ ℕ ℚ":
def qpow_example_5 : ℚ := (3 : ℕ) ^ 2

[Ruben Van de Velde]

Nat.card { p : M × M // p.1 * p.2 = p.2 * p.1 } / (Nat.card M : ℚ) ^ (2)

Sounds good

[Jireh Loreaux]

I assume in the first four cases it's casting to ℚ, and in the last case for some reason it fails to insert the coercion? I'm not sure what the issue is exactly.

[Jireh Loreaux]

Does it work if you add an ↑?

[Moritz Firsching]

def qpow_example_6 : ℚ := ↑3 ^ 2

works

[Thomas Murrills]

It would probably also work if you wrote something like ((3 ^ 2) : ℕ) or ((3^2) : ℕ) : ℚ); that way it knows to compute the power in ℕ, then cast. My guess is that this is more efficient (if that’s a concern here) since we get to just use Nat.pow.

As for what exactly the rules are for things like HPow.hPow and notations like ^, it’s a bit of a mystery to me as well…I’m not sure why it chooses some things in some cases or how I should know what to expect.