Zulip Chat Archive

Stream: maths

Topic: subalgebra.under

Yury G. Kudryashov (Oct 28 2021 at 17:53):

Am I right that docs#subalgebra.under is a special case of docs#subalgebra.restrict_scalars? If not, what's the difference?

Yury G. Kudryashov (Oct 28 2021 at 17:54):

If yes, then I suggest that we either completely remove subalgebra.under, or redefine it using restrict_scalars.

Johan Commelin (Oct 28 2021 at 17:57):

I think you are right.

Eric Wieser (Oct 28 2021 at 18:41):

Try redefining it with restrict_scalars, and if it works delete it?

Eric Wieser (Oct 31 2021 at 22:12):

#10080

Eric Wieser (Oct 31 2021 at 22:13):

I think actually removing it is more work, so I'm punting that to a follow-up

Eric Wieser (Nov 02 2021 at 12:43):

Alright, it's gone

Last updated: Dec 20 2023 at 11:08 UTC