mathlib3

e282089f - feat(linear_algebra/sesquilinear_form): preliminary results for nondegeneracy (#12269)

feat(linear_algebra/sesquilinear_form): preliminary results for nondegeneracy (#12269) Several lemmas needed to define nondegenerate bilinear forms and show that the canonical pairing of the algebraic dual is nondegenerate. Add domain restriction of bilinear maps in the second component and in both compenents. Some type-class generalizations for symmetric, alternating, and reflexive sesquilinear forms.