Theorems · Theorem · number theory

ClassGroup.norm_le

∀ {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) (a : S) {y : ℤ},
  (∀ (k : ι), abv ((bS.repr a) k) ≤ y) → abv ((Algebra.norm R) a) ≤ ClassGroup.normBound abv bS * y ^ Fintype.card ι

If the R-integral element a : S has coordinates ≤ y with respect to some basis b, its norm is less than normBound abv b * y ^ dim S.

Defined in

Mathlib.NumberTheory.ClassNumber.Finite

Cited by

1 results in Mathlib

Foundations

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

Assumes

EuclideanDomainCommRingIsDomainAlgebraDecidableEqFintype