Theorems · Definition · commutative algebra

IsGaloisGroup.mulSemiringActionOfNormal

(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] →
                  [FaithfulSMul B C] → [IsGaloisGroup (↥N) B C] → [N.Normal] → MulSemiringAction G B

If N is a normal subgroup of G and IsGaloisGroup N B C, then G acts on B as a MulSemiringAction, via the action defined in smulOfNormal.

Defined in

Mathlib.RingTheory.IsGaloisGroup.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupSemiringMulSemiringActionCommSemiringAlgebraFaithfulSMulIsGaloisGroupSubgroup.Normal