RationalCandidateRoots.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Rational roots of candidate representations

def OAI.JointDickman.shiftedCandidateRoot line 10
theorem OAI.JointDickman.shifted_numerator_coprime line 12
theorem OAI.JointDickman.shiftedCandidateRoot_fraction line 18

theorem OAI.JointDickman.shiftedCandidateRoot_injective line 27

Source documentation

Equal rational roots force equal reduced denominators and prescribe exactly the coefficient at any other position.

theorem shiftedCandidateRoot_injective {b c b' c' : ℕ} {i i' : ℤ}
    (hc : 0 < c) (hc' : 0 < c') (hbc : b.Coprime c) (hbc' : b'.Coprime c')
    (he : shiftedCandidateRoot b c i = shiftedCandidateRoot b' c' i') :
    c = c' ∧ (b' : ℤ) = b+(i'-i)*c := by
…

Mentions: OAI.JointDickman.shiftedCandidateRoot

theorem OAI.JointDickman.translated_candidate_coefficient_ne_zero line 44
Source documentation
A reduced coefficient with denominator greater than one can never vanish after translation by an integer multiple of that denominator.
```
theorem translated_candidate_coefficient_ne_zero {b c : ℕ}
    (hbc : b.Coprime c) (hc : 1 < c) (t : ℤ) : (b : ℤ)+t*c ≠ 0 := by
…
```