Theorems · Theorem · number theory

NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow

∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsFractionRing 𝒪 K] [inst_5 : IsDedekindDomain 𝒪] [CharZero 𝒪] [Module.Finite ℤ 𝒪] (L : Type u_3) (𝒪' : Type u_4)
  [inst_8 : Field L] [inst_9 : NumberField L] [inst_10 : CommRing 𝒪'] [inst_11 : Algebra 𝒪' L] [IsFractionRing 𝒪' L]
  [inst_13 : IsDedekindDomain 𝒪'] [CharZero 𝒪'] [inst_15 : Algebra K L] [inst_16 : Algebra 𝒪 𝒪'] [inst_17 : Algebra 𝒪 L]
  [IsScalarTower 𝒪 K L] [IsScalarTower 𝒪 𝒪' L] [inst_20 : Module.IsTorsionFree 𝒪 𝒪'] [inst_21 : Module.Free ℤ 𝒪']
  [Module.Finite ℤ 𝒪'] [Module.Finite 𝒪 𝒪'],
  (NumberField.discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (NumberField.discr K).natAbs ^ Module.finrank K L

Defined in

Mathlib.NumberTheory.NumberField.Discriminant.Different

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldCommRingAlgebraIsFractionRingIsDedekindDomainCharZeroModule.FiniteFieldNumberFieldCommRingAlgebraIsFractionRingIsDedekindDomainCharZeroAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerModule.IsTorsionFreeModule.FreeModule.FiniteModule.Finite