Theorems · Definition · commutative algebra

IsGaloisGroup.smulOfNormal

(G : Type u_1) →
  [inst : Group G] →
    (B : Type u_3) →
      (C : Type u_4) →
        [inst_1 : Semiring C] →
          [inst_2 : MulSemiringAction G C] →
            (N : Subgroup G) →
              [inst_3 : CommSemiring B] → [inst_4 : Algebra B C] → [N.Normal] → [IsGaloisGroup (↥N) B C] → SMul G B

If N is a normal subgroup of G and IsGaloisGroup N B C, then G acts on B. For g : G and x : B, g • x is the unique element of B whose image in C is g • algebraMap B C x, see algebraMap_smulOfNormal.

Defined in

Mathlib.RingTheory.IsGaloisGroup.Basic

Cited by

2 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice

Assumes

GroupSemiringMulSemiringActionCommSemiringAlgebraSubgroup.NormalIsGaloisGroup