Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 14:24 2b71c803

View on Github →

feat(linear_algebra/dual): add the dual map (#6807)

Estimated changes

Modified src/linear_algebra/dual.lean

added def linear_equiv.dual_map

added theorem linear_equiv.dual_map_apply

added theorem linear_equiv.dual_map_refl

added theorem linear_equiv.dual_map_symm

added theorem linear_equiv.dual_map_trans

added def linear_map.dual_map

added theorem linear_map.dual_map_apply

added theorem linear_map.dual_map_comp_dual_map

added theorem linear_map.dual_map_id

added theorem linear_map.findim_range_dual_map_eq_findim_range

added theorem linear_map.ker_dual_map_eq_dual_annihilator_range

added theorem linear_map.range_dual_map_eq_dual_annihilator_ker

added theorem linear_map.range_dual_map_le_dual_annihilator_ker