instance IdealFactorization.numberField_ringOfIntegers_ideal_ufm (K : Type u_1) [Field K] [NumberField K] : UniqueFactorizationMonoid (Ideal (NumberField.RingOfIntegers K))

theorem IdealFactorization.numberField_ideal_factorization (K : Type u_1) [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) (hI : I ≠ ⊥) : (∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, Prime P) ∧ Associated (UniqueFactorizationMonoid.normalizedFactors I).prod I

noncomputable def IdealFactorization.idealNorm {d : ℤ} [IsDomain (ℤ√d)] [IsDedekindDomain (ℤ√d)] [Module.Free ℤ (ℤ√d)] (I : Ideal (ℤ√d)) : ℕ

theorem IdealFactorization.ideal_mul_properties {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] : (∀ (I I' J : Ideal R), J ≠ ⊥ → I * J = I' * J → I = I') ∧ ∀ (I J : Ideal R), I ≤ J → ∃ (J' : Ideal R), I = J * J'

theorem IdealFactorization.ideal_is_lattice {R : Type u_1} [CommRing R] [IsDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] (I : Ideal R) (hI : I ≠ ⊥) : Module.Free ℤ ↥I ∧ Module.Finite ℤ ↥I ∧ Module.finrank ℤ ↥I = Module.finrank ℤ R

instance IdealFactorization.classGroup_finite (K : Type u_1) [Field K] [NumberField K] : Finite (ClassGroup (NumberField.RingOfIntegers K))

def IdealFactorization.IdealsSimilar {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I J : Ideal R) : Prop

theorem IdealFactorization.similar_mul_right {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I I' J : Ideal R} (h : IdealsSimilar I I') : IdealsSimilar (I * J) (I' * J)