eq_zero_of_mul_eq_self_right — Mathlib

English

Let α be a MonoidWithZero in which every nonzero a has a left inverse; then every nonzero a has a right inverse.

Русский

Пусть α — моноид с нулём, в котором каждый ненулевой элемент имеет левый обратный; тогда у каждого ненулевого элемента есть правый обратный.

LaTeX

$$$$ (\forall a \neq 0, \exists b, b a = 1) \Rightarrow (\forall a \neq 0, \exists b, a b = 1) $$$$

Lean4

/-- An element of a `CancelMonoidWithZero` fixed by right multiplication by an element other
than one must be zero. -/
theorem eq_zero_of_mul_eq_self_right (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 :=
  Classical.byContradiction fun ha => h₁ <| mul_left_cancel₀ ha <| h₂.symm ▸ (mul_one a).symm

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