Theorems · Definition · number theory

ClassGroup.cardM

{R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] →
      [inst_1 : CommRing S] →
        [IsDomain S] →
          [inst_3 : Algebra R S] →
            {abv : AbsoluteValue R ℤ} →
              {ι : Type u_5} → [DecidableEq ι] → [Fintype ι] → Module.Basis ι R S → abv.IsAdmissible → ℕ

If we have a large enough set of elements in R^ι, then there will be a pair whose remainders are close together. We'll show that all sets of cardinality at least cardM bS adm elements satisfy this condition. The value of cardM is not at all optimal: for specific choices of R, the minimum cardinality can be exponentially smaller.

Defined in

Mathlib.NumberTheory.ClassNumber.Finite

Cited by

4 results in Mathlib

Foundations

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

Assumes

EuclideanDomainCommRingIsDomainAlgebraDecidableEqFintype