eq_zero_or_eq_zero_of_kahler_eq_zero

English

If kahler x y = 0 then either x = 0 or y = 0.

Русский

Если kahler x y = 0, то либо x = 0, либо y = 0.

LaTeX

$$o.kahler x y = 0 \\Rightarrow x=0 \\lor y=0$$

Lean4

theorem eq_zero_or_eq_zero_of_kahler_eq_zero {x y : E} (hx : o.kahler x y = 0) : x = 0 ∨ y = 0 :=
  by
  have : ‖x‖ * ‖y‖ = 0 := by simpa [hx] using (o.norm_kahler x y).symm
  rcases eq_zero_or_eq_zero_of_mul_eq_zero this with h | h
  · left
    simpa using h
  · right
    simpa using h

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