Theorems · Theorem · field theory

Algebra.FormallyEtale.iff_exists_algEquiv_prod

∀ (K : Type u_1) (A : Type u) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] [Algebra.EssFiniteType K A],
  Algebra.FormallyEtale K A ↔ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

If A is an essentially of finite type algebra over a field K, then A is formally étale over K if and only if A is a finite product of separable field extensions.

Defined in

Mathlib.RingTheory.Etale.Field

Cited by

1 results in Mathlib

Foundations

Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCommRingAlgebraAlgebra.EssFiniteType