Étale field extensions

Mathlib's Algebra.FormallyEtale.of_isSeparable shows that a separable field extension is formally étale. This file adds the finiteness condition: a finite separable field extension is étale (Algebra.Etale.of_isSeparable).

theorem Algebra.Etale.of_isSeparable (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Module.Finite K L] [Algebra.IsSeparable K L] : Etale K L

A finite separable field extension is étale.