Commit 2023-05-07 21:39 b1c01758

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.