div_mul_cancel

Mathlib.Algebra.Group.Defs

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

English

a / b · b = a

Русский

a / b · b = a

LaTeX

$$$a / b \\cdot b = a$$$

Lean4

@[to_additive (attr := simp)]
theorem div_mul_cancel (a b : G) : a / b * b = a := by rw [div_eq_mul_inv, inv_mul_cancel_right a b]

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

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

Разделы

Аффилиация

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