mul_div_cancel_of_invertible

Mathlib.Algebra.GroupWithZero.Invertible

URI: https://scilib.ai/kg/mathlib#mul_div_cancel_of_invertible

English

In a GroupWithZero, for invertible b, a * b / b = a.

Русский

В группе с нулём, при обратимости b, a * b / b = a.

LaTeX

$$$a \\cdot b / b = a \\\\text{ for } b \\\\neq 0$$$

Lean4

@[simp]
theorem mul_div_cancel_of_invertible (a b : α) [Invertible b] : a * b / b = a :=
  mul_div_cancel_right₀ a (Invertible.ne_zero b)

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

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

Разделы

Аффилиация

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