@[simp]
theorem
NNReal.coe_expect
{ι : Type u_1}
(s : Finset ι)
(a : ι → NNReal)
:
↑(Finset.expect s fun (i : ι) => a i) = Finset.expect s fun (i : ι) => ↑(a i)
@[simp]
theorem
Complex.ofReal_expect
{ι : Type u_1}
(s : Finset ι)
(a : ι → ℝ)
:
↑(Finset.expect s fun (i : ι) => a i) = Finset.expect s fun (i : ι) => ↑(a i)
@[simp]
theorem
RCLike.coe_expect
{ι : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
(s : Finset ι)
(a : ι → ℝ)
:
↑(Finset.expect s fun (i : ι) => a i) = Finset.expect s fun (i : ι) => ↑(a i)