Theorem LinearMap.dualPairing_nondegenerate

Modification history

2026-04-28 19:12

Mathlib/LinearAlgebra/Dual/Lemmas.lean

chore(LinearAlgebra/Dual): deprecate `Module.dualPairing` (#37542) …

Deleted LinearMap.dualPairing_nondegenerate View on Github →

2023-05-21 22:16

Mathlib/LinearAlgebra/Dual.lean

feat: port LinearAlgebra.Dual (#3659)

Added LinearMap.dualPairing_nondegenerate View on Github →