Theorems · Theorem · number theory

FractionalIdeal.abs_det_basis_change

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  [inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R (nonZeroDivisors ℤ)) K] [inst_8 : Algebra ℚ K] [IsDomain K]
  {ι : Type u_3} [inst_10 : Fintype ι] [inst_11 : DecidableEq ι] (b : Module.Basis ι ℤ R)
  (I : FractionalIdeal (nonZeroDivisors R) K) (bI : Module.Basis ι ℤ ↥↑I),
  |(Module.Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K b).det (Subtype.val ∘ ⇑bI)| =
    FractionalIdeal.absNorm I

Defined in

Mathlib.RingTheory.FractionalIdeal.Norm

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainModule.FreeModule.FiniteCommRingAlgebraIsFractionRingIsLocalizationAlgebraIsDomainFintypeDecidableEq