Commit 2024-04-13 04:26 38a23fcc
View on Github →chore(RingTheory/IsTensorProduct): resolve porting note about simps! (#12092) Uncomment the simps configuration (which has to become simps!) and delete the generated lemma which was added manually. I verified that both are identical.