Forgetting type class structure on variables

Stream: new members

[Sebastian Monnet]

Suppose I have defined a finite field extension $L/K$, and now I want to use the same variable names for a result that doesn't require finiteness of the extension. Is there a way I can relax the assumption that $L/K$ is finite? Here's a very naive MWE where I fail to do this:

import field_theory.galois

variables (K L : Type*) [field K] [field L] [algebra K L] [finite_dimensional K L]

variables (L : Type*) [field L] [algebra K L]

[Kevin Buzzard]

Use sections?

import field_theory.galois

section fd_stuff

variables (K L : Type*) [field K] [field L] [algebra K L] [finite_dimensional K L]

end fd_stuff

section general_stuff

variables (K L : Type*) [field K] [field L] [algebra K L]

end general_stuff

[Kevin Buzzard]

Or even

import field_theory.galois

variables (K L : Type*) [field K] [field L] [algebra K L]

section fd_stuff

variable [finite_dimensional K L]

end fd_stuff

[Sebastian Monnet]

Okay, thanks!

[Anne Baanen]

Another approach is to name the variable and use include/omit:

import field_theory.galois

variables (K L : Type*) [field K] [field L] [algebra K L] [fd : finite_dimensional K L]

-- `fd` is not used implicitly

include fd

-- `fd` is used implicitly

omit fd

-- `fd` is not used implicitly

Note that named variables have slightly different behaviour: they are not automatically included.