Theorems · Definition · field theory

IntermediateField.toSubalgebra

{K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → IntermediateField K L → Subalgebra K L

Reinterpret an IntermediateField as a Subalgebra.

Defined in

Mathlib.FieldTheory.IntermediateField.Basic

Cited by

134 results in Mathlib

Foundations

Depth 46 from the axioms, rests on 391 definitions · uses propext, Quot.sound

Assumes

FieldFieldAlgebra