mul_div

Mathlib.Algebra.Group.Basic

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

English

In a division-monoid, a · (b / c) = a · b / c.

Русский

В моноиде с операцией деления выполняется a · (b / c) = a · b / c.

LaTeX

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

Lean4

@[to_additive]
theorem mul_div (a b c : G) : a * (b / c) = a * b / c := by simp only [mul_assoc, div_eq_mul_inv]

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

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

Разделы

Аффилиация

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