Theorems · Definition · field theory

RatFunc.Luroth.algEquiv

{K : Type u_1} → [inst : Field K] → {E : IntermediateField K (RatFunc K)} → E ≠ ⊥ → RatFunc K ≃ₐ[K] ↥E

The K-algebra equivalence between K⟮X⟯ and an intermediate field E given by sending X to generator E. See also Luroth.eq_adjoin_generator.

Defined in

Mathlib.FieldTheory.RatFunc.Luroth

Cited by

3 results in Mathlib

Foundations

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

Assumes

Field