div_mul_cancel_right

Mathlib.Algebra.Group.Basic

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

English

In any group G, for all a,b ∈ G, a / (b a) = b⁻¹.

Русский

В любой группе G для любых a,b ∈ G выполняется a / (b a) = b⁻¹.

LaTeX

$$$\forall a,b \in G,\ a/(b\,a) = b^{-1}.$$

Lean4

@[to_additive (attr := simp)]
theorem div_mul_cancel_right (a b : G) : a / (b * a) = b⁻¹ := by rw [← inv_div, mul_div_cancel_right]

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

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

Разделы

Аффилиация

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