Stream: new members

Topic: Syntax question: applying polynomial.exists_separable_of_ir

Jakob Scholbach (Mar 05 2021 at 16:15):

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 (Mar 05 2021 at 16:18):

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

#check polynomial.exists_separable_of_irreducible p irred fne0


Jakob Scholbach (Mar 05 2021 at 16:23):

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 (Mar 05 2021 at 16:25):

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 (Mar 05 2021 at 16:25):

Because you're likely working with a fixed p

Last updated: May 18 2021 at 17:44 UTC