Theorems · Inductive type · commutative algebra

IsGaloisGroup

(G : Type u_1) →
  (A : Type u_2) →
    (B : Type u_4) →
      [inst : Group G] →
        [inst_1 : CommSemiring A] → [inst_2 : Semiring B] → [Algebra A B] → [MulSemiringAction G B] → Prop

G is a Galois group for L/K if the action of G on L is faithful with fixed field K. In particular, we do not assume that L is an algebraic extension of K. See the implementation notes in this file for the meaning of this definition in the case of rings.

Defined in

Mathlib.RingTheory.IsGaloisGroup.Defs

Cited by

96 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 10 definitions · uses no axioms

Assumes

GroupCommSemiringSemiringAlgebraMulSemiringAction