Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-01 07:41 9ceb1141

View on Github →

feat(analysis/normed_space/inner_product): Define the inner product based on is_R_or_C (#4057)

Estimated changes

added theorem abs_norm_eq_norm
added theorem abs_inner_le_norm
added theorem abs_real_inner_le_norm
added def euclidean_space
added theorem findim_euclidean_space
added theorem inner_abs_conj_sym
added theorem inner_add_add_self
added theorem inner_add_left
added theorem inner_add_right
added theorem inner_conj_sym
added theorem inner_eq_zero_sym
added theorem inner_im_symm
added theorem inner_mul_conj_re_abs
added theorem inner_neg_left
added theorem inner_neg_neg
added theorem inner_neg_right
added structure inner_product_space.core
added theorem inner_re_symm
added theorem inner_re_zero_left
added theorem inner_re_zero_right
added theorem inner_self_abs_to_K
added theorem inner_self_conj
added theorem inner_self_eq_zero
added theorem inner_self_im_zero
added theorem inner_self_nonneg
added theorem inner_self_nonneg_im
added theorem inner_self_nonpos
added theorem inner_self_re_abs
added theorem inner_self_re_to_K
added theorem inner_smul_left
added theorem inner_smul_right
added theorem inner_sub_left
added theorem inner_sub_right
added theorem inner_sub_sub_self
added theorem inner_sum
added theorem inner_zero_left
added theorem inner_zero_right
added theorem norm_add_mul_self
added theorem norm_add_mul_self_real
added theorem norm_add_pow_two
added theorem norm_add_pow_two_real
added theorem norm_eq_sqrt_inner
added theorem norm_sub_mul_self
added theorem norm_sub_mul_self_real
added theorem norm_sub_pow_two
added theorem norm_sub_pow_two_real
added theorem parallelogram_law
added theorem real_inner_comm
added theorem real_inner_eq_re_inner
added theorem real_inner_self_abs
added theorem real_inner_self_nonneg
added theorem real_inner_self_nonpos
added theorem real_inner_smul_left
added theorem real_inner_smul_right
added theorem sum_inner
deleted theorem abs_inner_le_norm
deleted def bilin_form_of_inner
deleted def euclidean_space
deleted theorem findim_euclidean_space
deleted theorem inner_add_add_self
deleted theorem inner_add_left
deleted theorem inner_add_right
deleted theorem inner_add_sub_eq_zero_iff
deleted theorem inner_comm
deleted theorem inner_mul_inner_self_le
deleted theorem inner_neg_left
deleted theorem inner_neg_neg
deleted theorem inner_neg_right
deleted structure inner_product_space.core
deleted theorem inner_self_eq_norm_square
deleted theorem inner_self_eq_zero
deleted theorem inner_self_nonneg
deleted theorem inner_self_nonpos
deleted theorem inner_smul_left
deleted theorem inner_smul_right
deleted theorem inner_smul_self_left
deleted theorem inner_smul_self_right
deleted theorem inner_sub_left
deleted theorem inner_sub_right
deleted theorem inner_sub_sub_self
deleted theorem inner_sum
deleted theorem inner_zero_left
deleted theorem inner_zero_right
deleted theorem norm_add_mul_self
deleted theorem norm_add_pow_two
deleted theorem norm_sub_mul_self
deleted theorem norm_sub_pow_two
deleted theorem orthogonal_projection_def
deleted theorem orthogonal_projection_mem
deleted theorem parallelogram_law
deleted theorem submodule.Inf_orthogonal
deleted theorem submodule.inf_orthogonal
deleted theorem submodule.infi_orthogonal
deleted theorem submodule.mem_orthogonal'
deleted theorem submodule.mem_orthogonal
deleted theorem submodule.orthogonal_gc
deleted theorem submodule.orthogonal_le
deleted theorem sum_inner
added theorem is_R_or_C.I_im'
added theorem is_R_or_C.conj_div
added theorem is_R_or_C.conj_inv
modified theorem is_R_or_C.inv_def
added theorem is_R_or_C.norm_conj
modified theorem is_R_or_C.of_real_add
modified theorem is_R_or_C.of_real_mul
modified theorem is_R_or_C.of_real_neg
added theorem is_R_or_C.zero_re'
modified theorem is_R_or_C.zero_re
modified def euclidean_quadrant
added theorem sesq_form.map_sum_left