Documentation

Mathlib.NumberTheory.NumberField.House

House of an algebraic number #

This file defines the house of an algebraic number α, which is the largest of the modulus of its conjugates.

References #

Tagshouse #

number field, algebraic number, house

def NumberField.house {K : Type u_1} [Field K] [NumberField K] (α : K) :

The house of an algebraic number as the norm of its image by the canonical embedding.

Equations
Instances For
    theorem NumberField.house_eq_sup' {K : Type u_1} [Field K] [NumberField K] (α : K) :
    NumberField.house α = (Finset.univ.sup' fun (φ : K →+* ) => φ α‖₊)

    The house is the largest of the modulus of the conjugates of an algebraic number.

    theorem NumberField.house_sum_le_sum_house {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (s : Finset ι) (α : ιK) :
    NumberField.house (∑ is, α i) is, NumberField.house (α i)
    @[simp]
    theorem NumberField.house_intCast {K : Type u_1} [Field K] [NumberField K] (x : ) :
    NumberField.house x = |x|
    theorem NumberField.house.exists_ne_zero_int_vec_house_le (K : Type u_1) [Field K] [NumberField K] {α : Type u_2} {β : Type u_3} (a : Matrix α β (NumberField.RingOfIntegers K)) (ha : a 0) {p : } {q : } (h0p : 0 < p) (hpq : p < q) [Fintype β] (cardβ : Fintype.card β = q) {A : } (habs : ∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) A) [DecidableEq (K →+* )] [Fintype α] (cardα : Fintype.card α = p) :
    ∃ (ξ : βNumberField.RingOfIntegers K), ξ 0 a.mulVec ξ = 0 ∀ (l : β), NumberField.house (ξ l) NumberField.house.c₁ K * (NumberField.house.c₁ K * q * A) ^ (p / (q - p))

    There exists a "small" non-zero algebraic integral solution of an non-trivial underdetermined system of linear equations with algebraic integer coefficients.