Theorems · Definition · field theory

FixedBy.intermediateField

{M : Type u} →
  [inst : Monoid M] →
    (K : Type u_1) →
      (F : Type v) →
        [inst_1 : Field F] →
          [inst_2 : MulSemiringAction M F] →
            M → [inst_3 : Field K] → [inst_4 : Algebra K F] → [SMulCommClass M K F] → IntermediateField K F

The intermediate field between K and F fixed by the field endomorphism m.

Defined in

Mathlib.FieldTheory.Fixed

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidFieldMulSemiringActionFieldAlgebraSMulCommClass