English
If coordinates of an element a w.r.t. a basis have each absolute value below y, then the absolute norm is strictly less than normBound abv bS times y^|ι|.
Русский
Если все координаты a по базису имеют модуль меньшe y, то нормa строго меньше bound.
LaTeX
$$∀ y, coordinates ≤ y ⇒ |norm(a)| < normBound abv bS · y^{|ι|}$$
Lean4
/-- 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 ≤ norm_bound abv b * y ^ n`. (See also `norm_le` and `norm_lt`). -/
noncomputable def normBound : ℤ :=
let n := Fintype.card ι
let i : ι := Nonempty.some bS.index_nonempty
let m : ℤ :=
Finset.max' (Finset.univ.image fun ijk : ι × ι × ι => abv (Algebra.leftMulMatrix bS (bS ijk.1) ijk.2.1 ijk.2.2))
⟨_, Finset.mem_image.mpr ⟨⟨i, i, i⟩, Finset.mem_univ _, rfl⟩⟩
Nat.factorial n • (n • m) ^ n
