mathlib3
b0c71237 - chore(linear_algebra/tensor_product): make more lemmas dsimp-eligible (#18140)

Commit

2 years ago

chore(linear_algebra/tensor_product): make more lemmas dsimp-eligible (#18140) These are more items to add to the list in #18121

Author

eric-wieser

Parents