Documentation

AdeleRingLocallyCompact.RingTheory.DedekindDomain.Factorization

Factorization of ideals and fractional ideals of Dedekind domains #

This file includes finset versions of ideal factors.

source
theorem Ideal.finite_factors_of_nonZeroDivisor {R : Type u_1} [CommRing R] [IsDedekindDomain R] (r : ↥(nonZeroDivisors R)) :
{v : IsDedekindDomain.HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {↑r}}.Finite
source
@[reducible, inline]
abbrev Ideal.factorsFinset {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (h : I ≠ 0) :
Finset (IsDedekindDomain.HeightOneSpectrum R)
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Ideal.factorsFinset_of_nonZeroDivisor {R : Type u_1} [CommRing R] [IsDedekindDomain R] (r : ↥(nonZeroDivisors R)) :
    Finset (IsDedekindDomain.HeightOneSpectrum R)
    Equations
    Instances For