mul_inverse_cancel_left — Mathlib

English

Let x be a unit in a monoid with zero and let y be arbitrary. Then x · (x^{-1} · y) = y.

Русский

Пусть x является единицей в моноиде с нулём; тогда для произвольного y верно x · (x^{-1} · y) = y.

LaTeX

$$$\forall x,y\,\text{IsUnit}(x) \Rightarrow x\cdot\bigl(x^{-1}\cdot y\bigr) = y$$$

Lean4

theorem mul_inverse_cancel_left (x y : M₀) (h : IsUnit x) : x * (inverse x * y) = y := by
  rw [← mul_assoc, mul_inverse_cancel x h, one_mul]

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