Theorem RKHS.posSemidef_iff_re_sum_kernel'

Modification history

2026-09-01 23:21
Mathlib/Analysis/InnerProductSpace/Reproducing.lean
feat(Analysis/InnerProductSpace/Reproducing): add outerKernel (#42682) …
Added RKHS.posSemidef_iff_re_sum_kernel'View on Github →