Theorems · Theorem · field theory

InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois

∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  (A : Set Gal(K/k)), A ∈ nhds 1 ↔ ∃ L, ↑L.fixingSubgroup ⊆ A

Defined in

Mathlib.FieldTheory.Galois.Profinite

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsGalois