# Zulip Chat Archive

## 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
```

work in your context?

#### 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: Dec 20 2023 at 11:08 UTC