Theorems · Theorem · field theory

InfiniteGalois.mk_toAlgEquivAux

∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K)
  (L : FiniteGaloisIntermediateField k K) (hx' : InfiniteGalois.toAlgEquivAux✝ g x ∈ L.toIntermediateField)
  (hx : x ∈ L.toIntermediateField), ⟨InfiniteGalois.toAlgEquivAux✝ g x, hx'⟩ = ((InfiniteGalois.proj L) g) ⟨x, hx⟩

Defined in

Mathlib.FieldTheory.Galois.Profinite

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsGalois