Mathlib Changelog
v4
Changelog
About
Github
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