Commit 2023-05-24 08:50 cc9bb0f3

View on Github →

feat: port Analysis.Complex.Isometry (#4292)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Isometry.lean

added theorem LinearIsometry.im_apply_eq_im

added theorem LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re

added theorem LinearIsometry.re_apply_eq_re

added theorem LinearIsometry.re_apply_eq_re_of_add_conj_eq

added theorem det_rotation

added theorem linearEquiv_det_rotation

added theorem linear_isometry_complex

added theorem linear_isometry_complex_aux

added def rotation

added def rotationOf

added theorem rotationOf_rotation

added theorem rotation_apply

added theorem rotation_injective

added theorem rotation_ne_conjLie

added theorem rotation_symm

added theorem rotation_trans

added theorem toMatrix_rotation