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]