Theorems · Theorem · field theory

IsGaloisGroup.mulEquivCongr_mapSubgroup_fixingSubgroup

∀ (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'] (S : Set B),
  Subgroup.map (↑(IsGaloisGroup.mulEquivCongr G G' A B)) (fixingSubgroup G S) = fixingSubgroup G' S

Defined in

Mathlib.FieldTheory.Galois.IsGaloisGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupCommRingCommRingIsDomainAlgebraFaithfulSMulMulSemiringActionMulSemiringActionIsGaloisGroupIsGaloisGroupFiniteFinite