Commit 2023-02-16 17:18 5455cb0b
View on Github →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.
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.