Syntax question: applying polynomial.exists_separable_of_ir

Stream: new members

[Jakob Scholbach]

Another newbie syntax question: I am trying to make use of polynomial.exists_separable_of_irreducible. I manage to invoke it like in the following mwe:

variable p : ℕ
variable pprime : p.prime
variables (K : Type) [hK: field K]
variable hchar : char_p K p
variable f : polynomial K
variable irred : irreducible f
variable fne0 : f ≠ 0
#check @polynomial.exists_separable_of_irreducible K hK p pprime hchar f irred fne0

However, I can't seem to omit the input hK for example, even though (??) in the definition of polynomial.exists_separable_of_irreducible I thought it is not needed to specify it if it is an instance in the ambiant context like the one defined by the line ... [hk : field K]. So, conretely, what do I need to do prior to the invokation of polynomial.exists_separable_of_irreducible in order to let most assumptions be implicitly inferred from the context? Thanks!

[Yakov Pechersky]

You have to supply _all_ the arguments when you use @declnamehere. Does

#check polynomial.exists_separable_of_irreducible p irred fne0

work in your context?

[Jakob Scholbach]

Ah, thanks. Using your suggestion I get an error

p : ℕ,
pprime : nat.prime p,
K : Type,
hK : field K,
hchar : char_p K p,
f : polynomial K,
irred : irreducible f,
fne0 : f ≠ 0
⊢ fact (nat.prime p)

It does work if I replace it with variable pprime : fact p.prime though. What is the point of this fact?

[Yakov Pechersky]

fact places a hypothesis into the typeclass context like:

[fact p.prime]

Which is how I've seen it done in files that deal with fields over a prime p, so you don't have to carry and pass around the prime p hypothesis.

[Yakov Pechersky]

Because you're likely working with a fixed p