Commit 2023-09-27 03:37 ad44c68b

View on Github →

chore(RingTheory/TensorProduct): extra lemmas about {nat,int}Cast (#7391)

Estimated changes