Theorems · Theorem · number theory

NumberField.house.exists_ne_zero_int_vec_house_le

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)),
  a ≠ 0 →
    ∀ {p q : ℕ},
      0 < p →
        p < q →
          ∀ [inst_2 : Fintype β],
            Fintype.card β = q →
              ∀ {A : ℝ},
                (∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A) →
                  ∀ [inst_3 : DecidableEq (K →+* ℂ)] [inst_4 : Fintype α],
                    Fintype.card α = p →
                      ∃ ξ,
                        ξ ≠ 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.

Defined in

Mathlib.NumberTheory.NumberField.House

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldFintypeDecidableEqFintype