Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-26 13:34 66ec15cc

View on Github →

feat(analysis/complex/isometry): add linear_isometry_complex (#6923) add proof about the isometries in the complex plane

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem complex.conj_li_apply

Created src/analysis/complex/isometry.lean

added theorem linear_isometry.abs_apply_sub_one_eq_abs_sub_one

added theorem linear_isometry.im_apply_eq_im

added theorem linear_isometry.im_apply_eq_im_or_neg_of_re_apply_eq_re

added theorem linear_isometry.re_apply_eq_re

added theorem linear_isometry.re_apply_eq_re_of_add_conj_eq

added theorem linear_isometry_complex

added theorem linear_isometry_complex_aux

Modified src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry_equiv.linear_isometry.id_apply

added theorem linear_isometry_equiv.linear_isometry.id_to_linear_map

Modified src/data/complex/basic.lean

added theorem complex.conj_one

added theorem complex.conj_sub