Zulip Chat Archive
Stream: mathlib4
Topic: one-param struct for IsTensorProduct?
Kenny Lau (Nov 03 2025 at 12:38):
(context)
Should we make IsTensorProduct a one-param struct instead of a Prop? what is the general policy on this?
Christian Merten (Nov 03 2025 at 12:50):
I am in favour of making it a one-param struct, sometimes it gets unfolded accidentally and then anonymous dot notation gets confused.
Last updated: Dec 20 2025 at 21:32 UTC