mul_eq_zero_comm — Mathlib

English

In a setting with no zero divisors, the equation ab = 0 is equivalent to ba = 0 for elements a,b.

Русский

В окружении без нулевых делителей равенство ab = 0 эквивалентно ba = 0 для любых a,b.

LaTeX

$$$ab = 0 \iff ba = 0$$$

Lean4

/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` equals zero iff so is
`b * a`. -/
theorem mul_eq_zero_comm : a * b = 0 ↔ b * a = 0 :=
  mul_eq_zero.trans <| or_comm.trans mul_eq_zero.symm

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