feat(RingTheory): category of finite étale algebras over a separably closed field#38054

chrisflav wants to merge 3 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

chrisflav:finite-etale-sepclosedchrisflav/mathlib4:finite-etale-sepclosedCopy head branch name to clipboard