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

Estimated changes