Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-30 02:20 d28a163e

View on Github →

feat(linear_algebra/dual): define the algebraic dual pairing (#12827) We define the pairing of algebraic dual and show that it is nondegenerate.

Estimated changes