Mathlib Changelog
v4
Changelog
About
Github
Theorem
InnerProductSpace.continuousLinearMapOfBilin_zero
Modification history
2025-10-28 14:31
Mathlib/Analysis/InnerProductSpace/Dual.lean
feat: introduce covarianceBilin (#30324) …
Added
InnerProductSpace.continuousLinearMapOfBilin_zero
View on Github →