div_mul_cancel_of_invertible

Mathlib.Algebra.GroupWithZero.Invertible

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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