mul_ne_zero_comm

Mathlib.Algebra.GroupWithZero.Defs

URI: https://scilib.ai/kg/mathlib#mul_ne_zero_comm

← MathLib Explorer

English

In a zero-divisor-free structure, a*b ≠ 0 is equivalent to b*a ≠ 0.

Русский

В структуре без нулевых делителей a*b ≠ 0 эквивалентно b*a ≠ 0.

LaTeX

$$$ab \neq 0 \iff ba \neq 0$$$

Lean4

/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` is nonzero iff so is
`b * a`. -/
theorem mul_ne_zero_comm : a * b ≠ 0 ↔ b * a ≠ 0 :=
  mul_eq_zero_comm.not

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru