@[simp]

theorem indicator_one_inv {G : Type u_1} {M₀ : Type u_2} [One M₀] [Zero M₀] [Group G] (s : Set G) (a : G) : s⁻¹.indicator (fun (x : G) => 1) a = s.indicator (fun (x : G) => 1) a⁻¹

@[simp]

theorem indicator_one_neg {G : Type u_1} {M₀ : Type u_2} [One M₀] [Zero M₀] [AddGroup G] (s : Set G) (a : G) : (-s).indicator (fun (x : G) => 1) a = s.indicator (fun (x : G) => 1) (-a)