Theorems · Theorem · number theory

Int.Matrix.exists_ne_zero_int_vec_norm_le

∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ),
  Fintype.card α < Fintype.card β →
    0 < Fintype.card α →
      ∃ t,
        t ≠ 0 ∧
          A.mulVec t = 0 ∧
            ‖t‖ ≤ (↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))

Defined in

Mathlib.NumberTheory.SiegelsLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFintype