Zulip Chat Archive
Stream: mathlib4
Topic: nsmul/zsmul fields
Yury G. Kudryashov (Jul 02 2023 at 15:48):
@Sebastien Gouezel Could you please remind me why the current design with nsmul/zsmul fields is better than having •ℕ and •ℤ operations and not having a[AddCommMonoid M] : Module ℕ M as an instance?
Yury G. Kudryashov (Jul 02 2023 at 15:51):
The question is motivated by https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ModuleCat.2EisModule.20not.20defeq
Sebastien Gouezel (Jul 02 2023 at 17:45):
The thing is you really want to have the [AddCommMonoid M] : Module ℕ M instance (or the ℤ version), because when you do tensor products of groups you define them as tensor products of ℤ modules. This showed up in LTE, where there is a lot of back and forth between the two points of view.
Yury G. Kudryashov (Jul 02 2023 at 17:48):
Thank you!
Yury G. Kudryashov (Jul 02 2023 at 17:48):
OTOH, going back and forth is harder because one of the round-trips is not defeq.
Last updated: Dec 20 2023 at 11:08 UTC