Theorems · Definition · number theory

ClassGroup.finsetApprox

{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 → [Infinite R] → [DecidableEq R] → Finset R

finsetApprox is a finite set such that each fractional ideal in the integral closure contains an element close to finsetApprox.

Defined in

Mathlib.NumberTheory.ClassNumber.Finite

Cited by

9 results in Mathlib

Foundations

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

Assumes

EuclideanDomainCommRingIsDomainAlgebraDecidableEqFintypeInfiniteDecidableEq