@[implicit_reducible]

instance PUnit.instInnerProductSpace_meanFourier {𝕜 : Type u_1} [RCLike 𝕜] : InnerProductSpace 𝕜 PUnit.{u_2 + 1}

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PUnit.inner_eq_zero {𝕜 : Type u_1} [RCLike 𝕜] (x y : PUnit.{u_2 + 1}) : inner 𝕜 x y = 0