Commit 2025-11-12 21:15 13da915e

feat(NumberField): discriminant in disjoint extensions (#29943) We prove the following results:

• If K₁ and K₂ are linear disjoint number fields with coprime different ideals, then

(discr L).natAbs = (discr K₁).natAbs ^ Module.finrank ℚ K₂ * (discr K₂).natAbs ^ Module.finrank ℚ K₁ 

where L = K₁K₂.

• If K₁ and K₂ are number fields with coprime discriminant and K₁/ℚ Galois, then K₁ and K₂ are linear disjoint.