Theorem innerSL_real_flip

Modification history

2024-12-20 05:04
Mathlib/Analysis/InnerProductSpace/Basic.lean
chore(Analysis/InnerProductSpace): split large file (#20046) …
Modified innerSL_real_flipView on Github →
2024-04-05 06:15
Mathlib/Analysis/InnerProductSpace/Basic.lean
feat: `deriv` versions of composition lemmas with bilinear maps (#11868) …
Added innerSL_real_flipView on Github →