Theorems · Theorem · number theory

ClassGroup.exists_mem_finsetApprox

∀ {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] (a : S) {b : R},
  b ≠ 0 →
    ∃ q,
      ∃ r ∈ ClassGroup.finsetApprox bS adm,
        abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

We can approximate a / b : L with q / r, where r has finitely many options for L.

Defined in

Mathlib.NumberTheory.ClassNumber.Finite

Cited by

1 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EuclideanDomainCommRingIsDomainAlgebraDecidableEqFintypeInfiniteDecidableEq