mathlib3

d28a163e - feat(linear_algebra/dual): define the algebraic dual pairing (#12827)

feat(linear_algebra/dual): define the algebraic dual pairing (#12827) We define the pairing of algebraic dual and show that it is nondegenerate. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>