Theorem innerSL_real_flip

Modification history

2025-11-15 21:39
Mathlib/Analysis/InnerProductSpace/LinearMap.lean
chore(Analysis/InnerProductSpace/{Dual, LinearMap}): some renames (#31625) …
Deleted innerSL_real_flipView on Github →
2025-03-25 21:03
Mathlib/Analysis/InnerProductSpace/LinearMap.lean
refactor: remove duplicate `mul_comm` fields (#23289) …
Modified innerSL_real_flipView on Github →
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 →