Theorem RKHS.posSemidef_outerKernel

Modification history

2026-09-01 23:21

Mathlib/Analysis/InnerProductSpace/Reproducing.lean

feat(Analysis/InnerProductSpace/Reproducing): add outerKernel (#42682) …

Added RKHS.posSemidef_outerKernel View on Github →