mathlib3

36172d66 - feat(analysis/inner_product_space/symmetric): Polarization for `is_R_or_C` (#18397)

feat(analysis/inner_product_space/symmetric): Polarization for `is_R_or_C` (#18397) This PR contains * polarization identity for `is_R_or_C` for `T.is_symmetric` * `T.is_symmetric` implies `(∀ x, ⟪x, T x⟫ = 0) ↔ T = 0` Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>