English
A quadratic extension F ⊆ K is a normal extension. Equivalently, every irreducible polynomial over F that has a root in K splits completely over K.
Русский
Квадратичное расширение F ⊆ K является нормальным. Иными словами, каждый неприводимый многочлен над F, имеющий корень в K, распадается на линейные множители в K.
LaTeX
$$$K/F\ \text{is normal}$$$
Lean4
/-- A quadratic extension is normal.
-/
instance normal (F K : Type*) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] : Normal F K where
splits' := by
intro x
obtain h | h := le_iff_lt_or_eq.mp (finrank_eq_two F K ▸ minpoly.natDegree_le x)
· exact splits_of_natDegree_le_one _ (by rwa [Nat.le_iff_lt_add_one])
· exact splits_of_natDegree_eq_two _ h (minpoly.aeval F x)
