linear_ne_zero_of_im — Mathlib

English

Let cd: Fin 2 → ℝ, z ∈ ℂ with z.im ≠ 0, and h: cd ≠ 0. Then the linear combination (cd0) z + cd1 is nonzero for all i.

Русский

Пусть cd: Fin 2 → ℝ, z ∈ ℂ с z.im ≠ 0 и h: cd ≠ 0. Тогда линейная комбинация (cd0) z + cd1 не равна нулю.

LaTeX

$$$$ (cd_0) z + cd_1 \\neq 0. $$$$

Lean4

theorem linear_ne_zero_of_im {cd : Fin 2 → ℝ} {z : ℂ} (hz : z.im ≠ 0) (h : cd ≠ 0) : (cd 0 : ℂ) * z + cd 1 ≠ 0 :=
  by
  contrapose! h
  have : cd 0 = 0 := by
    -- we will need this twice

    apply_fun Complex.im at h
    simpa only [Complex.add_im, Complex.mul_im, Complex.ofReal_im, zero_mul, add_zero, Complex.zero_im, mul_eq_zero, hz,
      or_false] using h
  simp only [this, zero_mul, Complex.ofReal_zero, zero_add, Complex.ofReal_eq_zero] at h
  ext i
  fin_cases i <;> assumption

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