Theorems · Definition · field theory

FixedPoints.intermediateField

{F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (M : Type u_3) →
            [inst_3 : Monoid M] → [inst_4 : MulSemiringAction M E] → [SMulCommClass M F E] → IntermediateField F E

The intermediate field of fixed points fixed by a monoid action that commutes with the F-action on E.

Defined in

Mathlib.FieldTheory.Galois.Basic

Cited by

18 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraMonoidMulSemiringActionSMulCommClass