mathlib

c4926d76 - chore(ring_theory/is_tensor_product): golf a slow proof (#18169)

chore(ring_theory/is_tensor_product): golf a slow proof (#18169) This speeds it up by 7x according to `set_option profiler tt`, and is also shorter. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>