## Stream: new members

### Topic: degree of a field extension

#### Jack J Garzella (Jun 17 2020 at 02:25):

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 (Jun 17 2020 at 04:12):

@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


Last updated: May 11 2021 at 23:11 UTC