Zulip Chat Archive

Stream: new members

Topic: Looking for linear_algebra.direct_sum_module

Kevin Sullivan (Sep 23 2022 at 16:43):

I've updated to the most recent mathlib, and "import linear_algebra.direct_sum_module" is no longer working. Can anyone point me quickly and easily to the replacement? Thank you.

Patrick Massot (Sep 23 2022 at 16:47):

Did you try searching GitHub? https://github.com/leanprover-community/mathlib/search?q=direct_sum_module&type=commits

Patrick Massot (Sep 23 2022 at 16:47):

https://github.com/leanprover-community/mathlib/commit/afa31bed1b58a326af5584f1041fcbf9e57c3228 seems promising

Patrick Massot (Sep 23 2022 at 16:48):

Although the date is worrying

Patrick Massot (Sep 23 2022 at 16:48):

Are you really updating something that wasn't updated since January 2019?

Matt Diamond (Sep 23 2022 at 16:56):

it looks like the file wasn't actually renamed / moved in its entirety until August 2021: https://github.com/leanprover-community/mathlib/commit/aca0874a9ce95510752f4075f80f273172e9b177

Matt Diamond (Sep 23 2022 at 16:57):

so it's possible that Kevin is just using something that got left behind in that earlier move

Matt Diamond (Sep 23 2022 at 16:59):

either way, looks like algebra.direct_sum.module is the place to look

Patrick Massot (Sep 23 2022 at 17:01):

Ok, that makes more sense

Kevin Sullivan (Sep 26 2022 at 14:06):

Matt Diamond said:

either way, looks like algebra.direct_sum.module is the place to look

Thank you! --Kevin

Last updated: Dec 20 2023 at 11:08 UTC