Def ContinuousLinearMap.bilinearRestrictScalars

Modification history

2024-12-10 16:45

Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

feat(Analysis/Distribution): generalize linearity of SchwartzMap.bilinLeftCLM (#19823) …

Added ContinuousLinearMap.bilinearRestrictScalars View on Github →