left_inv_eq_right_inv — Mathlib

English

In a Monoid, if b·a = 1 and a·c = 1, then b = c.

Русский

В моноиде, если b·a = 1 и a·c = 1, то b = c.

LaTeX

$$$\\forall M\\,[Monoid M],\\forall a,b,c\\in M:\\ (b\\cdot a = 1) \\Rightarrow (a\\cdot c = 1) \\Rightarrow b=c$$$

Lean4

@[to_additive]
theorem left_inv_eq_right_inv (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
    -- This lemma is higher priority than later `zero_smul` so that the `simpNF` is happy

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