!4#4344 NumberTheory.Padics.Hensel

Stream: mathlib4

[Xavier Roblot]

Does parameter exist in Lean4? So far I have replaced those with variable but I get the feeling it is not a perfect replacement.

[David Loeffler]

I think use of parameter was already deprecated in mathlib3, wasn't it?

[Xavier Roblot]

In any case, it was still used in this file. So I replaced parameter with variable and it works well except for this definition

private def T : ℝ := ‖F.eval a / ((F.derivative.eval a ^ 2 : ℤ_[p]) : ℚ_[p])‖

Every time, T is used, I have to provide the implicit arguments otherwise it fails. I fixed this by using a local notation

private def T0 : ℝ := ‖F.eval a / ((F.derivative.eval a ^ 2 : ℤ_[p]) : ℚ_[p])‖

local notation "T" => @T0 p _ F a

but there is maybe a better way to proceed.

[Yaël Dillies]

Why don't you just make the uninferrable implicit arguments explicit?

[Xavier Roblot]

Yaël Dillies said:

Why don't you just make the uninferrable implicit arguments explicit?

But then I would have to write T p F a everywhere instead of T and T is used at a lot of places. Or am I missing something...

[Yaël Dillies]

Do you really need to add all those implicit arguments? I would expect you need add only one.

[Yaël Dillies]

At any rate, using local notation is perfectly acceptable.

[Johan Commelin]

The cool thing about Lean 4 is that you can also write T (p := p) F a whenever needed. If it's not too often, that might also be a nice strategy.