TensorProduct.curry

Stream: mathlib4

[Xavier Roblot]

In the port of TensorProduct.curry in RingTheory.TensorProduct, @[simps] has been changed to @[simps!]. As consequence, instead of docs#tensor_product.algebra_tensor_module.curry_apply in Mathlib3, we now have docs4#TensorProduct.AlgebraTensorModule.curry_apply_apply in Mathlib4.

Is it something that was intentional ?

[Chris Hughes]

I doubt it. My guess is that simps gave an error, so it was changed mindlessly to simps!.

[Xavier Roblot]

No, it works fine if I change back to @[simps] and lint does not give any error

[Yaël Dillies]

Probably it gave an error at some point.

[Xavier Roblot]

Yeah, I guess so.

Should I make a PR to change it back?

[Xavier Roblot]

Oh, there is also docs#tensor_product.algebra_tensor_module.mk_apply and docs4#TensorProduct.AlgebraTensorModule.mk_apply_apply .. but this one gives an error if I change it back to @[simps]

[Xavier Roblot]

!4#4995

I was not able though to solve the problem for docs4#TensorProduct.AlgebraTensorModule.mk. Putting a @[simps] instead of @[simps!] gives an error. However, the lemma docs#tensor_product.algebra_tensor_module.mk_apply isn't used anywhere in the library.

[Yury G. Kudryashov]

You can put simps! but list the projections you want. E.g., simps! apply.

[Xavier Roblot]

Oh great! Thanks!

[Xavier Roblot]

I have updated the PR !4#4995

[Yury G. Kudryashov]

Left a review.

[Xavier Roblot]

Thanks. I have made the changes