Theorems · Theorem · field theory

FixedPoints.mem_intermediateField_iff

∀ {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] [inst_5 : SMulCommClass M F E] {x : E},
  x ∈ FixedPoints.intermediateField M ↔ ∀ (m : M), m • x = x

Defined in

Mathlib.FieldTheory.Galois.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraMonoidMulSemiringActionSMulCommClass