Mathlib.Analysis.PSeries and HPow

Stream: mathlib4

[Michael Stoll]

Consider the following.

import Mathlib.Tactic
-- import Mathlib.Analysis.PSeries

variable (x : ℝ)

#check x ^ 2 -- hover over the `2` in the infoview
             -- with `import Mathlib.Analysis.PSeries`, it is `2 : ℝ`, else `2 : ℕ`.

It seems that importing Mathlib.Analysis.Pseries undoes the HPow fix.

[Eric Wieser]

The HPow fix isn't live yet

[Eric Wieser]

We currently have to fix it in every file that uses ^, and it's only fixed for that file

[Michael Stoll]

But how can it then be fixed without the import?

[Mauricio Collares]

I suspect exponentiation by a real number is not even defined without the import, so there is no confusion.