∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R] {x : R},
  (x ∈ ClassGroup.finsetApprox bS adm) =
    ∃ i j, i ≠ j ∧ (ClassGroup.distinctElems bS adm) i - (ClassGroup.distinctElems bS adm) j = x