Theorems · Theorem · field theory

Algebra.FormallyEtale.of_isSeparable_aux

∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L]
  [Algebra.EssFiniteType K L], Algebra.FormallyEtale K L

This is a weaker version of of_isSeparable that additionally assumes EssFiniteType K L. Use that instead. This is Iversen Corollary II.5.3.

Defined in

Mathlib.RingTheory.Etale.Field

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraAlgebra.IsSeparableAlgebra.EssFiniteType