lambda_dvd_mul_sub_one_mul_sub_eta_add_one

English

If λ divides x−1, then λ^4 divides x^3−1.

Русский

Если λ делит x−1, тогда λ^4 делит x^3−1.

LaTeX

$$$\lambda \mid (x-1) \Rightarrow \lambda^{4} \mid (x^{3}-1)$$$

Lean4

/-- We have that `λ` divides `x * (x - 1) * (x - (η + 1))`. -/
theorem lambda_dvd_mul_sub_one_mul_sub_eta_add_one : λ ∣ x * (x - 1) * (x - (η + 1)) :=
  by
  rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h
  · exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h _) _
  · exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h _) _
  · refine dvd_mul_of_dvd_right ?_ _
    rw [show x - (η + 1) = x + 1 - (η - 1 + 3) by ring]
    exact dvd_sub h <| dvd_add dvd_rfl hζ.toInteger_sub_one_dvd_prime'

Похожие утверждения