mul_ne_zero_iff — Mathlib

English

Let A be a structure with no zero divisors. Then for every a,b in A, ab ≠ 0 if and only if both a ≠ 0 and b ≠ 0.

Русский

Пусть A — структура без нулевых делителей. Тогда для любых a,b ∈ A выполняется: ab ≠ 0 тогда и только тогда, когда a ≠ 0 и b ≠ 0.

LaTeX

$$$ab \neq 0 \iff a \neq 0 \land b \neq 0$$$

Lean4

/-- If `α` has no zero divisors, then the product of two elements is nonzero iff both of them
are nonzero. -/
theorem mul_ne_zero_iff : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 :=
  mul_eq_zero.not.trans not_or

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