eq_zero_of_mul_eq_self_left — Mathlib

English

In a CancelMonoidWithZero, if b ≠ 1 and a * b = a, then a = 0.

Русский

В CancelMonoidWithZero, если b ≠ 1 и a b = a, то a = 0.

LaTeX

$$$$ b \neq 1 \land a b = a \Rightarrow a = 0 $$$$

Lean4

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

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