Cyclotomic extension of finite field

theorem FiniteField.isCyclotomicExtension_iff_isAlgClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Finite K] : IsCyclotomicExtension {n : ℕ | ↑n ≠ 0} K L ↔ IsAlgClosure K L