lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd

English

λ divides x(x−1)(x−(η+1)).

Русский

λ делит произведение x(x−1)(x−(η+1)).

LaTeX

$$$\lambda \mid x( x-1 )( x-(\eta+1) )$$$

Lean4

/-- If `λ` does not divide `x`, then `λ ^ 4` divides `x ^ 3 - 1` or `x ^ 3 + 1`. -/
theorem lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd {x : 𝓞 K} (h : ¬λ ∣ x) :
    λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1 :=
  by
  rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with H | H | H
  · contradiction
  · left
    exact lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ H
  · right
    exact lambda_pow_four_dvd_cube_add_one_of_dvd_add_one hζ H

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