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

source
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
    source
    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.

    source
    theorem NumberField.house_sum_le_sum_house {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (s : Finset ι) (α : ι → K) :
    NumberField.house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, NumberField.house (α i)
    source
    theorem NumberField.house_nonneg {K : Type u_1} [Field K] [NumberField K] (α : K) :
    0 ≤ NumberField.house α
    source
    theorem NumberField.house_mul_le {K : Type u_1} [Field K] [NumberField K] (α : K) (β : K) :
    NumberField.house (α * β) ≤ NumberField.house α * NumberField.house β
    source
    @[simp]
    theorem NumberField.house_intCast {K : Type u_1} [Field K] [NumberField K] (x : ℤ) :
    NumberField.house ↑x = ↑|x|
    source
    theorem NumberField.house.basis_repr_abs_le_const_mul_house (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] (α : NumberField.RingOfIntegers K) (i : K →+* ℂ) :
    Complex.abs ↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr ↑α) i) ≤ NumberField.house.c K * NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) α)
    source
    theorem NumberField.house.exists_ne_zero_int_vec_house_le (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] [DecidableEq α] (a : Matrix α β (NumberField.RingOfIntegers K)) (ha : a ≠ 0) {p : ℕ} {q : ℕ} (cardα : Fintype.card α = p) (cardβ : Fintype.card β = q) (h0p : 0 < p) (hpq : p < q) {A : ℝ} (habs : ∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A) :
    ∃ (ξ : β → 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.