Zulip Chat Archive

Stream: mathlib4

Topic: !4#3649 RingTheory.TensorProduct

Eric Wieser (Apr 30 2023 at 10:54):

This one is running into very unpleasant typeclass issues; baseChange_sub has an ext line that should be finding TensorProduct.AlgebraTensorModule.curry_injective, but it doesn't find it. Attempting to write out the refine line manually takes an unpleasantly long time to elaborate

Eric Wieser (Apr 30 2023 at 11:06):

Bizarrely, I now get a timeout on the @[simp]

Last updated: May 02 2025 at 03:31 UTC