solution_spec' — Mathlib

English

A reformulation: (solution p a1 a2)^{p} a1_0 = (solution p a1 a2) a2_0, i.e., s^{p} a1_0 = s a2_0.

Русский

Переформулировка: (solution p a1 a2)^{p} a1_0 = (solution p a1 a2) a2_0, то есть s^{p} a1_0 = s a2_0.

LaTeX

$$(solution(p,a1,a2))^{p} * a1.coeff 0 = solution(p,a1,a2) * a2.coeff 0$$

Lean4

theorem solution_spec' {a₁ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (a₂ : 𝕎 k) :
    solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0 :=
  by
  have := solution_spec p a₁ a₂
  obtain ⟨q, hq⟩ := Nat.exists_eq_succ_of_ne_zero hp.out.ne_zero
  have hq' : q = p - 1 := by simp only [hq, tsub_zero, Nat.succ_sub_succ_eq_sub]
  conv_lhs =>
    congr
    congr
    · skip
    · rw [hq]
  rw [pow_succ', hq', this]
  field_simp

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