∀ (G : Type u_2) (F : Type u_3) [inst : Group G] [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G]
  [FaithfulSMul G F], Function.Bijective (MulSemiringAction.toAlgHom (↥(FixedPoints.subfield G F)) F)