Eric Wieser (Jul 06 2021 at 19:48):
Looking at docs#semi_normed_space and docs#normed_space, I'm reminded of
module - the objects are identical, the only difference is unused typeclass arguments. Should we remove the latter and rename the former to replace it?
cc @Rémy Degenne, since you seem to be embarking on a generalization in this area.
Riccardo Brasca (Jul 06 2021 at 19:54):
I don't remember what happened with
semimodule, but I think we really want both notions, and there are theorems that we can state for
semi_normed_space that hold only for
Eric Wieser (Jul 06 2021 at 19:55):
Right, but there are no theorems which are true for
[normed_group M] [normed_space R M] but not
[normed_group M] [semi_normed_space R M]
Eric Wieser (Jul 06 2021 at 19:57):
Just as there are no theorems true for the old
[ring R] [add_comm_group M] [module R M] but not
[ring R] [add_comm_group M] [semimodule R M]
Riccardo Brasca (Jul 06 2021 at 20:00):
Ah yes, there is another layer coming from
Eric Wieser (Jul 07 2021 at 08:19):
Eric Wieser (Jan 14 2022 at 22:28):
6 months later, and CI passes in the branch :tada:!
Eric Wieser (Jan 14 2022 at 22:29):
Would have been much easier if people didn't keep proving more and more things on top of
Yaël Dillies (Jan 14 2022 at 22:29):
Oh lol, I'm working on some myself right now.
Yaël Dillies (Feb 03 2022 at 09:42):
Yaël Dillies (Feb 03 2022 at 09:45):
cc @Riccardo Brasca
Riccardo Brasca (Feb 03 2022 at 09:46):
I've never really tried to understand what
normed_add_torsor means in mathlib, so I don't have any opinion, but I guess that if they're now the same thing we case delete one of them.
Yaël Dillies (Feb 03 2022 at 11:34):
Eric Wieser (Feb 03 2022 at 16:24):
Nice find, but good luck fighting CI
Yaël Dillies (Feb 03 2022 at 16:25):
I have good hope that torsors are less widely used than normed groups or modules!
Yaël Dillies (Feb 04 2022 at 20:17):
seminormed_add_torsor has been terminated :robot:
Last updated: Aug 03 2023 at 10:10 UTC