mathlib3

b4f03bc5 - fix(analysis/inner_product_space/basic): restore `bilin_form_of_real_inner` (#18093)

fix(analysis/inner_product_space/basic): restore `bilin_form_of_real_inner` (#18093) I was using this downstream as `bilin_form_of_real_inner.to_quadratic_form`, and I don't see a clear replacement. Until we have api connecting sesquilinear forms with quadratic forms, we should not remove `bilin_form` API. This partially reverts #15780.