mathlib

b1c01758 - refactor(linear_algebra/dual): make `module.dual` reducible (#18963)

refactor(linear_algebra/dual): make `module.dual` reducible (#18963) Otherwise Lean 4 can't apply `simp` lemmas about linear maps to elements of `module.dual`. There is no need for this to be reducible anyway, as all the instances on `dual` agree with the instances on linear maps. Also delete `basis.to_dual_equiv_symm_apply`, which stated `⇑(b.to_dual_equiv.symm) f = ⇑((linear_equiv.of_injective b.to_dual _).symm) (⇑((linear_equiv.of_top (linear_map.range b.to_dual) _).symm) f)` which was hardly helpful. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>