div_eq_div_mul_div

Mathlib.Algebra.Group.Basic

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

English

In a commutative group, a / b = c / b * (a / c).

Русский

В коммутативной группе a / b = c / b * (a / c).

LaTeX

$$$\forall a,b,c\in G,\ a / b = c / b * (a / c)$$$

Lean4

@[to_additive]
theorem div_eq_div_mul_div (a b c : G) : a / b = c / b * (a / c) := by simp [mul_left_comm c]

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

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

Разделы

Аффилиация

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