divp_assoc

Mathlib.Algebra.Group.Units.Defs

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

English

Partial division distributes over multiplication: (a · b) /ₚ u = a · (b /ₚ u).

Русский

Частичное деление распределяется по умножению: (a · b) /ₚ u = a · (b /ₚ u).

LaTeX

$$$ (a \cdot b) /ₚ u = a \cdot (b /ₚ u) $$$

Lean4

theorem divp_assoc (a b : α) (u : αˣ) : a * b /ₚ u = a * (b /ₚ u) :=
  mul_assoc _ _ _

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

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

Разделы

Аффилиация

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