Theorems · Theorem · field theory

InfiniteGalois.toAlgEquivAux_eq_proj_of_mem

∀ {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 : x ∈ L.toIntermediateField),
  InfiniteGalois.toAlgEquivAux✝ g x = ↑(((InfiniteGalois.proj L) g) ⟨x, hx⟩)

Defined in

Mathlib.FieldTheory.Galois.Profinite

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsGalois