Theorems · Theorem · field theory

Algebra.Etale.iff_exists_algEquiv_prod

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

A is étale over a field K if and only if A is a finite product of finite separable field extensions.

Defined in

Mathlib.RingTheory.Etale.Field

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebra