theorem indicate_wInner_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [DecidableEq ι] [RCLike 𝕜] (s : Finset ι) (f : ι → 𝕜) : RCLike.wInner 1 (𝟭 s) f = ∑ i ∈ s, f i

theorem wInner_one_indicate {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [DecidableEq ι] [RCLike 𝕜] (f : ι → 𝕜) (s : Finset ι) : RCLike.wInner 1 f (𝟭 s) = ∑ i ∈ s, (starRingEnd 𝕜) (f i)

theorem mu_wInner_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [DecidableEq ι] [RCLike 𝕜] (s : Finset ι) (f : ι → 𝕜) : RCLike.wInner 1 (mu s) f = s.expect fun (i : ι) => f i

theorem wInner_one_mu {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [DecidableEq ι] [RCLike 𝕜] (f : ι → 𝕜) (s : Finset ι) : RCLike.wInner 1 f (mu s) = s.expect fun (i : ι) => (starRingEnd 𝕜) (f i)