Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-17 08:54 b4f03bc5

View on Github →

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.

Estimated changes