feat(linear_algebra/sesquilinear_form): Add is_refl for sesq_form.is_alt (#10341)
feat(linear_algebra/sesquilinear_form): Add is_refl for sesq_form.is_alt (#10341)

Lemma `is_refl` shows that an alternating sesquilinear form is reflexive.
Refactored `sesquilinear_form` in a similar way as `bilinear_form` will be in #10338.







leanprover-community/mathlib,leanprover-community/mathlib