mul_inverse_cancel_right

Mathlib.Algebra.GroupWithZero.Units.Basic

URI: https://scilib.ai/kg/mathlib#Ring.mul_inverse_cancel_right

English

If x is a unit, then y · x · x^{-1} = y for all y.

Русский

Если x — единица, то y · x · x^{-1} = y для всех y.

LaTeX

$$$\forall y:\, y \cdot x \cdot x^{-1} = y$ при $IsUnit(x)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru