mul_eq_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_eq_left (h : IsUnit a) : a * b = a ↔ b = 1 :=
  calc
    a * b = a ↔ a * b = a * 1 := by rw [mul_one]
    _ ↔ b = 1 := by rw [h.mul_right_inj]

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