Theorems · Theorem · number theory

NumberField.linearDisjoint_of_isGalois_isCoprime_discr

∀ (L : Type u_3) [inst : Field L] [inst_1 : NumberField L] (K₁ K₂ : IntermediateField ℚ L) [IsGalois ℚ ↥K₁],
  IsCoprime (NumberField.discr ↥K₁) (NumberField.discr ↥K₂) → K₁.LinearDisjoint ↥K₂

Let K₁ and K₂ be two number fields and assume that K₁/ℚ is Galois. If discr K₁ and discr K₂ are coprime, then they are linear disjoint over ℚ.

Defined in

Mathlib.NumberTheory.NumberField.Discriminant.Different

Cited by

1 results in Mathlib

Foundations

Depth 317 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberFieldIsGalois