Commit 2023-11-02 21:53 7f7a1f04
View on Github →chore(RingTheory/TensorProduct): missing trivial lemmas (#8120) This also tweaks some argument explicitness, and removes unnecessary type ascriptions
chore(RingTheory/TensorProduct): missing trivial lemmas (#8120) This also tweaks some argument explicitness, and removes unnecessary type ascriptions