mul_div_assoc

Mathlib.Algebra.Group.Defs

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

English

For all a,b,c in G, a·b / c = a·(b / c).

Русский

Для любых a,b,c в G выполняется a·b / c = a·(b / c).

LaTeX

$$$a \\cdot b / c = a \\cdot (b / c)$$$

Lean4

@[to_additive]
theorem mul_div_assoc (a b c : G) : a * b / c = a * (b / c) := by rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]

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

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

Разделы

Аффилиация

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