right_ne_mul

Mathlib.Algebra.Group.Basic

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

English

Let M be a monoid with the right cancellation property. For all a, b in M, b ≠ a·b iff a ≠ 1.

Русский

Пусть M — моноид, обладающий правым отменением. Для любых a, b в M выполняется: b ≠ a·b ↔ a ≠ 1.

LaTeX

$$$\forall a,b \in M,\ b \neq a b \iff a \neq 1$$$

Lean4

@[to_additive]
theorem right_ne_mul : b ≠ a * b ↔ a ≠ 1 :=
  right_eq_mul.not

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

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

Разделы

Аффилиация

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