Theorems · Theorem · commutative algebra

IsGaloisGroup.smul_mem_of_normal

∀ (G : Type u_1) (B : Type u_3) [inst : Group G] [inst_1 : Semiring B] [inst_2 : MulSemiringAction G B] {C : Type u_4}
  [inst_3 : CommSemiring C] [inst_4 : Algebra C B] (N : Subgroup G) [hN : N.Normal] [hC : IsGaloisGroup (↥N) C B]
  (g : G) (x : C), g • (algebraMap C B) x ∈ Set.range ⇑(algebraMap C B)

Defined in

Mathlib.RingTheory.IsGaloisGroup.Basic

Cited by

2 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext

Assumes

GroupSemiringMulSemiringActionCommSemiringAlgebraSubgroup.NormalIsGaloisGroup