Commit 2023-05-04 09:41 07992a1d

chore(analysis/inner_product_space/basic): golf the proof of Cauchy-Schwarz (#18938)

API changes

• Add inner_product_space.to_core.
• Make inner_product_space.core extend has_inner.
• Rename namespace from inner_product_space.of_core to inner_product_space.core.
• Rename inner_product_space.of_core.inner_norm_sq_eq_inner_self to inner_product_space.core.coe_norm_sq_eq_inner_self.
• Add inner_product_space.core.norm_inner_symm.
• Add inner_product_space.core.cauchy_schwarz_aux, use it to golf the proof of the Cauchy-Schwarz inequality and its versions.
• Use norm instead of is_R_or_C.abs here and there, the rest will migrate in #18919.
• Rename inner_product_space.of_core.abs_inner_le_norm to inner_product_space.core.norm_inner_le_norm, use norm.
• Add norm_inner_eq_norm_tfae and inner_eq_norm_mul_iff_div.
• Rename abs_inner_div_norm_mul_norm_eq_one_iff to norm_inner_div_norm_mul_norm_eq_one_iff, use norm.
• Rename inner_eq_norm_mul_iff_of_norm_one to inner_eq_one_iff_of_norm_one.