mathlib

5455cb0b - chore(linear_algebra/dual): prove a lemma with rfl (#18444)

chore(linear_algebra/dual): prove a lemma with rfl (#18444) I was surprised that `dsimp` didn't clean this up for me. The proof that used to be here was certainly not interesting.