∀ {F : Type u_2} [inst : Field F] {E : Type u_1} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (x : ↥K) (y : ↥(IntermediateField.fixedField K.fixingSubgroup)) (ϕ : ↥K.fixingSubgroup), ϕ • (↑x * ↑y) = ↑x * ↑y