Documentation

Atlas.NumberTheoryI.code.IdealFactorization

source
theorem finsuppProd_primeIdealPow_ne_zero {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (exps : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) :
(exps.prod fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℤ) => ↑v.asIdeal ^ e) ≠ 0
source
noncomputable def countFinsupp {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) :
IsDedekindDomain.HeightOneSpectrum R →₀ ℤ
Instances For
    source
    theorem finsuppProd_countFinsupp_eq {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) :
    ((countFinsupp K I).prod fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℤ) => ↑v.asIdeal ^ e) = ↑I
    source
    noncomputable def fractionalIdeal_mulEquiv_finsupp {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] :
    (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃* Multiplicative (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)
    Instances For
      source
      theorem fractionalIdeal_mulEquiv_finsupp_apply {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) (v : IsDedekindDomain.HeightOneSpectrum R) :
      (Multiplicative.toAdd ((fractionalIdeal_mulEquiv_finsupp K) I)) v = FractionalIdeal.count K v ↑I
      source
      theorem fractionalIdeal_mulEquiv_finsupp_symm_apply {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (exps : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) :
      ↑((fractionalIdeal_mulEquiv_finsupp K).symm (Multiplicative.ofAdd exps)) = exps.prod fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℤ) => ↑v.asIdeal ^ e
      source
      @[deprecated fractionalIdeal_mulEquiv_finsupp (since := "2025-05-04")]
      def Theorem_3_11 {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] :
      (FractionalIdeal (nonZeroDivisors R) K)ˣ ≃* Multiplicative (IsDedekindDomain.HeightOneSpectrum R →₀ ℤ)

      Alias of fractionalIdeal_mulEquiv_finsupp.

      Instances For
        source
        @[deprecated fractionalIdeal_mulEquiv_finsupp_apply (since := "2025-05-04")]
        theorem Theorem_3_11_forward_apply {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) (v : IsDedekindDomain.HeightOneSpectrum R) :
        (Multiplicative.toAdd ((fractionalIdeal_mulEquiv_finsupp K) I)) v = FractionalIdeal.count K v ↑I

        Alias of fractionalIdeal_mulEquiv_finsupp_apply.

        source
        @[deprecated fractionalIdeal_mulEquiv_finsupp_symm_apply (since := "2025-05-04")]
        theorem Theorem_3_11_inverse_apply {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (exps : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ) :
        ↑((fractionalIdeal_mulEquiv_finsupp K).symm (Multiplicative.ofAdd exps)) = exps.prod fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℤ) => ↑v.asIdeal ^ e

        Alias of fractionalIdeal_mulEquiv_finsupp_symm_apply.