Mathlib v3 is deprecated. Go to Mathlib v4

Theorem innerSL_flip_apply

Modification history

2023-03-19 08:24
src/analysis/inner_product_space/basic.lean
chore(analysis/inner_product_space/basic): explicit `π•œ` argument for `innerβ‚›β‚—` and `innerSL` (#18613) …
Modified innerSL_flip_applyView on Github β†’
2023-03-14 13:51
src/analysis/inner_product_space/basic.lean
chore(analysis/inner_product_space/basic): make arguments explicit (#18579) …
Modified innerSL_flip_applyView on Github β†’
2021-12-24 16:32
src/analysis/inner_product_space/basic.lean
feat(analysis/inner_product_space/adjoint): define the adjoint of a continuous linear map between Hilbert spaces (#10825) …
Added innerSL_flip_applyView on Github β†’