Theorems · Theorem · field theory

IsGaloisGroup.mulEquivCongr_symm_apply_smul

∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra A B] [inst_6 : FaithfulSMul A B]
  [inst_7 : MulSemiringAction G B] [inst_8 : MulSemiringAction G' B] [inst_9 : IsGaloisGroup G A B]
  [inst_10 : IsGaloisGroup G' A B] [inst_11 : Finite G] [inst_12 : Finite G'] (g : G') (x : B),
  (IsGaloisGroup.mulEquivCongr G G' A B).symm g • x = g • x

Defined in

Mathlib.FieldTheory.Galois.IsGaloisGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupCommRingCommRingIsDomainAlgebraFaithfulSMulMulSemiringActionMulSemiringActionIsGaloisGroupIsGaloisGroupFiniteFinite