degree of a field extension

Stream: new members

[Jack J Garzella]

I am trying to prove a theorem about degree two extensions (that they are all normal). I've proved most of it in a lemma called splits_of_degree_two_root.
The only thing stopping me from proving the theorem is that I don't have any idea how to state it. How would I formalize the notion of "a field extension of degree two"?

[Johan Commelin]

@Jack J Garzella I would do something like (modulo missing imports):

variables {K L : Type*} [field K] [field L] [algebra K L] [finite_dimensional K L]

lemma some_name (h : findim K L = 2) : some_statement