@[simp]

theorem conjneg_indicator_one {G : Type u_1} {R : Type u_2} [CommSemiring R] [StarRing R] [AddCommGroup G] (s : Set G) : conjneg (s.indicator fun (x : G) => 1) = (-s).indicator fun (x : G) => 1