PrimitiveVector.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Primitive rational vectors

A denominator and an integer coordinate vector are primitive if they have no common natural divisor greater than one. Multiplying such a vector by an integer not divisible by its denominator leaves a nonintegral coordinate. Every such coordinate stays at least the reciprocal denominator from every integer.

def OAI.QuantitativeVanDerWaerden.PrimitiveVector line 27
Source documentation
The denominator and all coordinates have no nontrivial common divisor.
```
def PrimitiveVector {ι : Type uIndex} (h : ℕ) (t : ι → ℤ) : Prop :=
…
```
theorem OAI.QuantitativeVanDerWaerden.PrimitiveVector.of_congr line 31
Source documentation
Changing coordinates by multiples of the denominator preserves primitivity.
```
theorem PrimitiveVector.of_congr {ι : Type uIndex} {h : ℕ} {T t : ι → ℤ}
    (hp : PrimitiveVector h T)
    (hcongr : ∀ i, ∃ z : ℤ, T i - t i = (h : ℤ) * z) :
    PrimitiveVector h t := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.PrimitiveVector
theorem OAI.QuantitativeVanDerWaerden.PrimitiveVector.of_sum_congr_mul line 47
Source documentation
Coordinates congruent to a common integer multiple of the first vector do not add a new obstruction to its primitivity.
```
theorem PrimitiveVector.of_sum_congr_mul {ι : Type uIndex} {h : ℕ} {T S : ι → ℤ}
    (hp : PrimitiveVector h (Sum.elim T S)) (a : ℤ)
    (hcongr : ∀ i, ∃ z : ℤ, S i = a * T i + (h : ℤ) * z) :
    PrimitiveVector h T := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.PrimitiveVector

theorem OAI.QuantitativeVanDerWaerden.PrimitiveVector.exists_not_dvd_mul line 64

Source documentation

Primitivity forces some multiplied coordinate to remain nonintegral.

theorem PrimitiveVector.exists_not_dvd_mul {ι : Type uIndex} [Fintype ι]
    {h : ℕ} {t : ι → ℤ} (hp : PrimitiveVector h t) (hh : 0 < h)
    {a : ℤ} (ha : ¬ (h : ℤ) ∣ a) : ∃ i, ¬ (h : ℤ) ∣ a * t i := by
…

Mentions: OAI.QuantitativeVanDerWaerden.PrimitiveVector

theorem OAI.QuantitativeVanDerWaerden.rational_separation line 86

Source documentation

A nonintegral rational with denominator h is separated from every integer.

theorem rational_separation {h : ℕ} (hh : 0 < h) {b : ℤ}
    (hb : ¬ (h : ℤ) ∣ b) (z : ℤ) :
    1 / (h : ℝ) ≤ |(b : ℝ) / (h : ℝ) - (z : ℝ)| := by
…

theorem OAI.QuantitativeVanDerWaerden.PrimitiveVector.exists_separated_coordinate line 101

Source documentation

A primitive vector has a coordinate separated from every integer translate.

theorem PrimitiveVector.exists_separated_coordinate {ι : Type uIndex} [Fintype ι]
    {h : ℕ} {t : ι → ℤ} (hp : PrimitiveVector h t) (hh : 0 < h)
    {a : ℤ} (ha : ¬ (h : ℤ) ∣ a) :
    ∃ i, ∀ z : ℤ, 1 / (h : ℝ) ≤ |(a : ℝ) * (t i : ℝ) / h - z| := by
…

Mentions: OAI.QuantitativeVanDerWaerden.PrimitiveVector