mathlib

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

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`. Co-authored-by: Johan Commelin <johan@commelin.net>