vecMulVec_eq_zero — Mathlib

English

If α has zero divisors and is a MulZeroClass, vecMulVec a b = 0 iff a = 0 or b = 0.

Русский

Если α имеет нулевые делители и является MulZeroClass, то vecMulVec a b = 0 тогда и только тогда, когда a = 0 или b = 0.

LaTeX

$$vecMulVec a b = 0 \\iff a = 0 \\lor b = 0$$

Lean4

@[simp]
theorem vecMulVec_eq_zero [MulZeroClass α] [NoZeroDivisors α] {a b : n → α} : vecMulVec a b = 0 ↔ a = 0 ∨ b = 0 := by
  simp only [← ext_iff, vecMulVec_apply, zero_apply, mul_eq_zero, funext_iff, Pi.zero_apply, forall_or_left,
    forall_or_right]

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