solution_nonzero — Mathlib

English

If a1_0 ≠ 0 and a2_0 ≠ 0, then the base solution is nonzero.

Русский

Если a1_0 ≠ 0 и a2_0 ≠ 0, то базовый коэффициент решения не равен нулю.

LaTeX

$$solution(p,a1,a2) ≠ 0$$

Lean4

theorem solution_nonzero {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : solution p a₁ a₂ ≠ 0 :=
  by
  intro h
  have := solution_spec p a₁ a₂
  rw [h, zero_pow] at this
  · simpa [ha₁, ha₂] using _root_.div_eq_zero_iff.mp this.symm
  · exact Nat.sub_ne_zero_of_lt hp.out.one_lt

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