big subfield is algebra over small subfield

Stream: Is there code for X?

[Aaron Liu]

If I have a two subfields A ≤ B, what's the way to construct the obvious Algebra A B?

[Junyan Xu]

There are Subfield.extendScalars and IntermediateField.extendScalars

[Aaron Liu]

In this case I think I really want to have the same subfield though...

[Aaron Liu]

I'll see if I can make this work.

[Junyan Xu]

You can also look at how IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin works. (In hindsight the smul field defeq could be better ...)

[Eric Wieser]

I think using inclusion h |>.toAlgebra ends up safe here

[Junyan Xu]

Oh indeed, defining smul to be defeq to multiplication on the ambient type is what we want here ...