divp_assoc'

Mathlib.Algebra.Group.Units.Defs

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

English

A variant form of associativity: a · (b /ₚ u) = (a · b) /ₚ u.

Русский

Вариант ассоциативности: a · (b /ₚ u) = (a · b) /ₚ u.

LaTeX

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

Lean4

@[deprecated divp_assoc (since := "2025-08-25")]
theorem divp_assoc' (x y : α) (u : αˣ) : x * (y /ₚ u) = x * y /ₚ u :=
  (divp_assoc _ _ _).symm

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

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

Разделы

Аффилиация

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