∀ {B : Type u_2} [inst : CommRing B] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G B] (H : Subgroup G)
  [inst_3 : H.Normal] (q : Quotient (QuotientGroup.leftRel H)) (x y : ↥(FixedPoints.subring B ↥H)),
  q • (x * y) = q • x * q • y