theorem indicator_one_wInner_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] (s : Finset ι) (f : ι → 𝕜) : RCLike.wInner 1 ((↑s).indicator fun (x : ι) => 1) f = ∑ i ∈ s, f i

theorem wInner_one_indicator_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] (f : ι → 𝕜) (s : Finset ι) : RCLike.wInner 1 f ((↑s).indicator fun (x : ι) => 1) = ∑ i ∈ s, (starRingEnd 𝕜) (f i)

theorem mu_wInner_one {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [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 ι] [RCLike 𝕜] (f : ι → 𝕜) (s : Finset ι) : RCLike.wInner 1 f (mu s) = s.expect fun (i : ι) => (starRingEnd 𝕜) (f i)