Mathlib v3 is deprecated. Go to Mathlib v4

Def module.dual_pairing

Modification history

2022-03-30 02:20
src/linear_algebra/dual.lean
feat(linear_algebra/dual): define the algebraic dual pairing (#12827) …
Added module.dual_pairingView on Github →