Theorem innerₗ_apply_apply

Modification history

2025-12-27 10:33
Mathlib/Analysis/InnerProductSpace/Basic.lean
chore: deprecate duplicate declaration for the scalar product as a sesquilinear form (#33316) …
Modified innerₗ_apply_applyView on Github →
2025-11-15 21:39
Mathlib/Analysis/InnerProductSpace/LinearMap.lean
chore(Analysis/InnerProductSpace/{Dual, LinearMap}): some renames (#31625) …
Added innerₗ_apply_applyView on Github →