mul_eq_right — Mathlib

English

Let M be a monoid and b a unit. Then for every a in M, a·b = b if and only if a = 1.

Русский

Пусть M — моноид, а b — единичный элемент. Тогда для каждого a в M выполняется a·b = b тогда и только тогда, когда a = 1.

LaTeX

$$$$\forall M [Monoid\ M], \forall a,b\in M,\ IsUnit(b) \Rightarrow (a\,b = b \ \Leftrightarrow\ a = 1).$$$$

Lean4

@[to_additive]
theorem mul_eq_right (h : IsUnit b) : a * b = b ↔ a = 1 :=
  calc
    a * b = b ↔ a * b = 1 * b := by rw [one_mul]
    _ ↔ a = 1 := by rw [h.mul_left_inj]

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