@[simp]

theorem Set.conj_indicator_one_apply {α : Type u_1} {R : Type u_2} [CommSemiring R] [StarRing R] (s : Set α) (a : α) : (starRingEnd R) (s.indicator (fun (x : α) => 1) a) = s.indicator (fun (x : α) => 1) a

@[simp]

theorem Set.conj_indicator_one {α : Type u_1} {R : Type u_2} [CommSemiring R] [StarRing R] (s : Set α) : (starRingEnd (α → R)) (s.indicator fun (x : α) => 1) = s.indicator fun (x : α) => 1