Finite reduced algebras over perfect fields

A finite reduced commutative algebra over a perfect field is étale. This permits finite affine quotients to be recognized as finite étale schemes from their coordinate algebras.

theorem TauCeti.algebraEtale_of_finite_of_isReduced (k : Type u_1) (A : Type u_2) [Field k] [PerfectField k] [CommRing A] [Algebra k A] [Module.Finite k A] [IsReduced A] : Algebra.Etale k A

A finite reduced commutative algebra over a perfect field is étale.