lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_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_sub_one_of_dvd_sub_one {x : 𝓞 K} (h : λ ∣ x - 1) : λ ^ 4 ∣ x ^ 3 - 1 :=
  by
  obtain ⟨y, hy⟩ := h
  have : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (η + 1))) := by
    calc
      _ = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (η + 1)) := by simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring
      _ = _ := by rw [hy]; ring
  rw [this, pow_succ]
  exact mul_dvd_mul_left _ (lambda_dvd_mul_sub_one_mul_sub_eta_add_one hζ y)

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