divRight_eq_mulRight_inv

Mathlib.Algebra.Group.Units.Equiv

URI: https://scilib.ai/kg/mathlib#Equiv.divRight_eq_mulRight_inv

English

For any a in G, the right-division by a is the same as right-multiplication by a⁻¹.

Русский

Для любого a∈G деление справа на a совпадает с умножением справа на a⁻¹.

LaTeX

$$$\\mathrm{divRight}(a) = \\mathrm{mulRight}(a^{-1})$$$

Lean4

@[to_additive]
theorem divRight_eq_mulRight_inv (a : G) : Equiv.divRight a = Equiv.mulRight a⁻¹ :=
  ext fun _ => div_eq_mul_inv _ _

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

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

Разделы

Аффилиация

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