Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-18 20:21 e282089f

View on Github →

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.

Estimated changes