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) :
      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) :
      house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, house (α i)
      source
      theorem NumberField.house_nonneg {K : Type u_1} [Field K] [NumberField K] (α : K) :
      0 ≤ house α
      source
      theorem NumberField.house_mul_le {K : Type u_1} [Field K] [NumberField K] (α β : K) :
      house (α * β) ≤ house α * house β
      source
      @[simp]
      theorem NumberField.house_intCast {K : Type u_1} [Field K] [NumberField K] (x : ℤ) :
      house ↑x = ↑|x|
      source
      theorem NumberField.house.basis_repr_norm_le_const_mul_house (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] (α : RingOfIntegers K) (i : K →+* ℂ) :
      ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤ NumberField.house.c✝ K * house ((algebraMap (RingOfIntegers K) K) α)
      source
      @[deprecated NumberField.house.basis_repr_norm_le_const_mul_house (since := "2025-02-17")]
      theorem NumberField.house.basis_repr_abs_le_const_mul_house (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] (α : RingOfIntegers K) (i : K →+* ℂ) :
      ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤ NumberField.house.c✝ K * house ((algebraMap (RingOfIntegers K) K) α)

      Alias of NumberField.house.basis_repr_norm_le_const_mul_house.

      source
      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 α β (RingOfIntegers K)) (ha : a ≠ 0) {p q : ℕ} (h0p : 0 < p) (hpq : p < q) [Fintype β] (cardβ : Fintype.card β = q) {A : ℝ} (habs : ∀ (k : α) (l : β), house ((algebraMap (RingOfIntegers K) K) (a k l)) ≤ A) [DecidableEq (K →+* ℂ)] [Fintype α] (cardα : Fintype.card α = p) :
      ∃ (ξ : β → RingOfIntegers K), ξ ≠ 0 ∧ a.mulVec ξ = 0 ∧ ∀ (l : β), 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.