lambda_pow_four_dvd_c_cube — Mathlib

English

λ^4 divides c^3 for S'; i.e. S'.c^3 is multiple of λ^4.

Русский

λ^4 делит c^3 для S'

LaTeX

$$$\lambda^4 \mid S'.c^3$$$

Lean4

/-- Given `S' : Solution'`, we have that `λ ^ 4` divides `S'.c ^ 3`. -/
theorem lambda_pow_four_dvd_c_cube : λ ^ 4 ∣ S'.c ^ 3 := by
  rcases a_cube_b_cube_congr_one_or_neg_one S' with ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ | ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ <;>
    · refine ⟨S'.u⁻¹ * (x + y), ?_⟩
      symm
      calc
        _ = S'.u⁻¹ * (λ ^ 4 * x + λ ^ 4 * y) := by ring
        _ = S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy]; ring
        _ = S'.u⁻¹ * (S'.u * S'.c ^ 3) := by rw [S'.H]
        _ = S'.c ^ 3 := by simp

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