lambda_pow_four_dvd_cube_add_one_of_dvd_add_one

English

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

Русский

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

LaTeX

$$$\lambda^4 \mid x^3 + 1$$$

Lean4

/-- If `λ` divides `x + 1`, then `λ ^ 4` divides `x ^ 3 + 1`. -/
theorem lambda_pow_four_dvd_cube_add_one_of_dvd_add_one {x : 𝓞 K} (h : λ ∣ x + 1) : λ ^ 4 ∣ x ^ 3 + 1 :=
  by
  replace h : λ ∣ -x - 1 := by
    convert h.neg_right using 1
    exact (neg_add' x 1).symm
  convert (lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ h).neg_right using 1
  ring

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