x in subobject (O(K)) -> (x : K) in subobject K

Stream: Is there code for X?

[Eric Rodriguez]

this is fairly easy to prove directly, but I'm not too sure if I'm missing a sensible generalization/if it's already there in that generalization (reaching the ends of my maths knowledge here!).

[Alex J. Best]

What is x? And what are these ideals of? In my experience just putting type ascriptions on a set for an ideal doesn't always determine what type the ideal is

[Eric Rodriguez]

I just realised I wasn't thinking about ideals, but subalgebras... the idea is the same regardless, it's meant to be that ideals/subwhateverobjects restricted to O(K) are just the pointwise restriction

[Eric Rodriguez]

(I want to prove is_cyclotomic_extension S K L -> is_cyclotomic_extension S O(K) O(L))