Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 01:48 1ddb93a9

View on Github →

feat(analysis/normed_space): define linear isometries (#5867)

define linear_isometry and linear_isometry_equiv;
add linear_map.ker_eq_bot_of_inverse;
replace inv_fun_apply lemmas with inv_fun_eq_symm;
golf some proofs in linear_algebra/finite_dimensional.

Estimated changes

Modified src/algebra/algebra/basic.lean

deleted theorem alg_equiv.inv_fun_apply

added theorem alg_equiv.inv_fun_eq_symm

Modified src/algebra/module/linear_map.lean

deleted theorem linear_equiv.inv_fun_apply

added theorem linear_equiv.inv_fun_eq_symm

Modified src/analysis/complex/basic.lean

modified def complex.continuous_linear_map.of_real

deleted theorem complex.continuous_linear_map.of_real_isometry

modified theorem complex.continuous_of_real

added theorem complex.isometry_of_real

added def complex.linear_isometry.of_real

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/inner_product.lean

added theorem im_inner_eq_norm_sub_I_smul_mul_self_sub_norm_add_I_smul_mul_self_div_four

added theorem inner_eq_sum_norm_sq_div_four

added theorem linear_equiv.coe_isometry_of_inner

added def linear_equiv.isometry_of_inner

added theorem linear_equiv.isometry_of_inner_to_linear_equiv

added theorem linear_isometry.inner_map_map

added theorem linear_isometry_equiv.inner_map_map

added theorem linear_map.coe_isometry_of_inner

added def linear_map.isometry_of_inner

added theorem linear_map.isometry_of_inner_to_linear_map

added theorem re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two

added theorem re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four

added theorem re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two

Created src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry.coe_comp

added theorem linear_isometry.coe_fn_injective

added theorem linear_isometry.coe_id

added theorem linear_isometry.coe_mul

added theorem linear_isometry.coe_one

added theorem linear_isometry.coe_to_continuous_linear_map

added theorem linear_isometry.coe_to_linear_map

added def linear_isometry.comp

added theorem linear_isometry.comp_assoc

added theorem linear_isometry.comp_continuous_iff

added theorem linear_isometry.comp_id

added theorem linear_isometry.diam_image

added theorem linear_isometry.diam_range

added theorem linear_isometry.dist_map

added theorem linear_isometry.ediam_image

added theorem linear_isometry.ediam_range

added theorem linear_isometry.edist_map

added theorem linear_isometry.ext

added def linear_isometry.id

added theorem linear_isometry.id_comp

added theorem linear_isometry.map_add

added theorem linear_isometry.map_eq_iff

added theorem linear_isometry.map_ne

added theorem linear_isometry.map_smul

added theorem linear_isometry.map_sub

added theorem linear_isometry.map_zero

added theorem linear_isometry.nnnorm_map

added theorem linear_isometry.norm_map

added def linear_isometry.to_continuous_linear_map

added theorem linear_isometry.to_linear_map_injective

added structure linear_isometry

added theorem linear_isometry_equiv.apply_symm_apply

added theorem linear_isometry_equiv.coe_inv

added theorem linear_isometry_equiv.coe_mk

added theorem linear_isometry_equiv.coe_mul

added theorem linear_isometry_equiv.coe_one

added theorem linear_isometry_equiv.coe_refl

added theorem linear_isometry_equiv.coe_symm_to_linear_equiv

added theorem linear_isometry_equiv.coe_symm_trans

added theorem linear_isometry_equiv.coe_to_linear_equiv

added theorem linear_isometry_equiv.coe_trans

added theorem linear_isometry_equiv.diam_image

added theorem linear_isometry_equiv.dist_map

added theorem linear_isometry_equiv.ediam_image

added theorem linear_isometry_equiv.edist_map

added theorem linear_isometry_equiv.ext

added theorem linear_isometry_equiv.map_add

added theorem linear_isometry_equiv.map_eq_iff

added theorem linear_isometry_equiv.map_eq_zero_iff

added theorem linear_isometry_equiv.map_ne

added theorem linear_isometry_equiv.map_smul

added theorem linear_isometry_equiv.map_sub

added theorem linear_isometry_equiv.map_zero

added theorem linear_isometry_equiv.nnnorm_map

added theorem linear_isometry_equiv.norm_map

added def linear_isometry_equiv.of_bounds

added def linear_isometry_equiv.refl

added theorem linear_isometry_equiv.refl_trans

added def linear_isometry_equiv.symm

added theorem linear_isometry_equiv.symm_apply_apply

added theorem linear_isometry_equiv.symm_symm

added theorem linear_isometry_equiv.symm_trans

added def linear_isometry_equiv.to_continuous_linear_equiv

added def linear_isometry_equiv.to_isometric

added theorem linear_isometry_equiv.to_linear_equiv_injective

added def linear_isometry_equiv.to_linear_isometry

added def linear_isometry_equiv.trans

added theorem linear_isometry_equiv.trans_assoc

added theorem linear_isometry_equiv.trans_refl

added theorem linear_isometry_equiv.trans_symm

added structure linear_isometry_equiv

Modified src/analysis/normed_space/mazur_ulam.lean

deleted def isometric.to_real_linear_equiv

deleted def isometric.to_real_linear_equiv_of_map_zero

deleted theorem isometric.to_real_linear_equiv_symm_apply

added def isometric.to_real_linear_isometry_equiv

added def isometric.to_real_linear_isometry_equiv_of_map_zero

added theorem isometric.to_real_linear_isometry_equiv_symm_apply

Modified src/analysis/normed_space/operator_norm.lean

deleted theorem add_monoid_hom.isometry_of_norm

added theorem continuous_linear_map.isometry_iff_norm

deleted theorem continuous_linear_map.isometry_iff_norm_image_eq_norm

added theorem linear_isometry.norm_to_continuous_linear_map

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.I_mul_re

Modified src/linear_algebra/basic.lean

added theorem linear_map.ker_eq_bot_of_inverse

Modified src/linear_algebra/finite_dimensional.lean

added theorem linear_equiv.coe_of_injective_endo

modified theorem linear_equiv.of_injective_endo_left_inv

modified theorem linear_equiv.of_injective_endo_right_inv

deleted theorem linear_equiv.of_injective_endo_to_fun

Modified src/topology/metric_space/isometry.lean

added theorem add_monoid_hom.isometry_iff_norm

added theorem add_monoid_hom.isometry_of_norm

modified theorem isometric.coe_mul

modified theorem isometric.mul_apply