kahler_ne_zero_iff — Mathlib

English

kahler x y ≠ 0 iff x ≠ 0 and y ≠ 0.

Русский

kahler x y ≠ 0 тогда и только тогда x ≠ 0 и y ≠ 0.

LaTeX

$$o.kahler x y \\neq 0 \\iff x \\neq 0 \\land y \\neq 0$$

Lean4

theorem kahler_ne_zero_iff (x y : E) : o.kahler x y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0 :=
  by
  refine ⟨?_, fun h => o.kahler_ne_zero h.1 h.2⟩
  contrapose
  simp only [not_and_or, Classical.not_not, kahler_apply_apply, Complex.real_smul]
  rintro (rfl | rfl) <;> simp

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