def IdealEquivalence.IsEquivalent (𝒪 : Subring ℂ) (L₁ L₂ : ComplexLattice.ProperIdeal 𝒪) : Prop

Two proper ideals L₁, L₂ of an order 𝒪 ⊆ ℂ are equivalent if they are equivalent as complex lattices in the sense of ComplexLattice.IsEquivalent.

theorem IdealEquivalence.IsEquivalent.refl (𝒪 : Subring ℂ) (L : ComplexLattice.ProperIdeal 𝒪) : IsEquivalent 𝒪 L L

Reflexivity of ideal equivalence: every proper ideal is equivalent to itself.

theorem IdealEquivalence.IsEquivalent.symm {𝒪 : Subring ℂ} {L₁ L₂ : ComplexLattice.ProperIdeal 𝒪} (h : IsEquivalent 𝒪 L₁ L₂) : IsEquivalent 𝒪 L₂ L₁

Symmetry of ideal equivalence: L₁ ~ L₂ implies L₂ ~ L₁.

theorem IdealEquivalence.IsEquivalent.trans {𝒪 : Subring ℂ} {L₁ L₂ L₃ : ComplexLattice.ProperIdeal 𝒪} (h₁₂ : IsEquivalent 𝒪 L₁ L₂) (h₂₃ : IsEquivalent 𝒪 L₂ L₃) : IsEquivalent 𝒪 L₁ L₃

Transitivity of ideal equivalence: L₁ ~ L₂ and L₂ ~ L₃ imply L₁ ~ L₃.

theorem IdealEquivalence.isEquivalent_equivalence (𝒪 : Subring ℂ) : Equivalence (IsEquivalent 𝒪)

IsEquivalent 𝒪 is an equivalence relation on proper ideals of 𝒪.

def IdealEquivalence.properIdealSetoid (𝒪 : Subring ℂ) : Setoid (ComplexLattice.ProperIdeal 𝒪)

The setoid on proper ideals of 𝒪 whose equivalence relation is ideal equivalence. Quotienting by this setoid produces the ideal class group.

def IdealEquivalence.IdealClassGroup (𝒪 : Subring ℂ) : Type

The ideal class group of an order 𝒪 ⊆ ℂ, defined as the quotient of the set of proper ideals by ideal equivalence.

def IdealEquivalence.IdealClassGroup.mk (𝒪 : Subring ℂ) (L : ComplexLattice.ProperIdeal 𝒪) : IdealClassGroup 𝒪

The canonical map sending a proper ideal L to its class in the ideal class group.

theorem IdealEquivalence.IdealClassGroup.mk_eq_mk_iff (𝒪 : Subring ℂ) (L₁ L₂ : ComplexLattice.ProperIdeal 𝒪) : mk 𝒪 L₁ = mk 𝒪 L₂ ↔ IsEquivalent 𝒪 L₁ L₂

Two proper ideals have the same ideal class iff they are equivalent.

def IdealEquivalence.idealClassGroupEquiv (𝒪 : Subring ℂ) : IdealClassGroup 𝒪 ≃ ComplexLattice.IdealClassGroup 𝒪

The ideal class group built from IsEquivalent agrees with the analogous quotient ComplexLattice.IdealClassGroup 𝒪 defined in the lattice setting.

@[reducible]

noncomputable def IdealEquivalence.IdealClassGroup.commGroup (𝒪 : Subring ℂ) : CommGroup (IdealClassGroup 𝒪)

The ideal class group of 𝒪 inherits a commutative group structure from the corresponding lattice ideal class group via idealClassGroupEquiv.

theorem IdealEquivalence.IdealClassGroup.finite (𝒪 : Subring ℂ) : Finite (IdealClassGroup 𝒪)

The ideal class group of an order 𝒪 ⊆ ℂ is finite.

noncomputable def IdealEquivalence.classNumber (𝒪 : Subring ℂ) : ℕ

The class number of an order 𝒪 ⊆ ℂ, defined as the cardinality of its ideal class group.