Theorem Module.dualMap_dualMap_eq_iff_of_injective

Modification history

2025-03-07 22:53

Mathlib/LinearAlgebra/Dual/Defs.lean

chore(LinearAlgebra): split long file `Dual.lean` (#22697) …

Modified Module.dualMap_dualMap_eq_iff_of_injective View on Github →

2024-10-31 02:17

Mathlib/LinearAlgebra/Dual.lean

feat (RootSystem/Hom): endomorphisms and automorphisms of root pairings (#18025) …

Added Module.dualMap_dualMap_eq_iff_of_injective View on Github →