mathlib3
1023d812 - chore(ring_theory/tensor_product): squeeze simps in a slow proof (#9671)

Commit

4 years ago

chore(ring_theory/tensor_product): squeeze simps in a slow proof (#9671) This proof just timed out in bors. Goes from 21s to 1s on my computer just by squeezing the simps.

Author

sgouezel

Parents

a132d0ab

mathlib3 1023d812 - chore(ring_theory/tensor_product): squeeze simps in a slow proof (#9671)

mathlib3
1023d812 - chore(ring_theory/tensor_product): squeeze simps in a slow proof (#9671)