Theorems · Definition · number theory

ClassGroup.normBound

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

If b is an R-basis of S of cardinality n, then normBound abv b is an integer such that for every R-integral element a : S with coordinates ≤ y, we have Algebra.norm a ≤ normBound abv b * y ^ n. (See also norm_le and norm_lt).

Defined in

Mathlib.NumberTheory.ClassNumber.Finite

Cited by

5 results in Mathlib

Foundations

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

Assumes

EuclideanDomainCommRingIsDomainAlgebraDecidableEqFintype