Theorem complex.isometry_euclidean_apply_one
Modification history
2022-09-30 21:28
src/analysis/inner_product_space/pi_L2.lean
feat(analysis/inner_product/orientation, geometry/euclidean/oriented_angle): use bundled orthonormal bases (#16475) …
Deleted complex.isometry_euclidean_apply_oneView on Github →2021-09-30 02:06
src/analysis/inner_product_space/pi_L2.lean
refactor(analysis/normed_space/{dual, pi_Lp}): split out inner product space parts (#9388) …
Modified complex.isometry_euclidean_apply_oneView on Github →