Commit 2025-10-09 13:58 cc0d5cbb

feat(IsCyclotomicExtension): some results for the sub-algebra case (#29665) We add some results about cyclotomic extensions which are also contained in an extension A ⊆ B of rings. In this case, the cyclotomic extension IsCyclotomicExtension S A C is determined by S and thus we can prove various statements such as the fact that the compositum of A[ζₙ] and A[ζₘ] is A[ζₗ] where l is the lcm of n and m.