right_distrib_equiv

Mathlib.SetTheory.Game.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.right_distrib_equiv

← MathLib Explorer

English

Right distributive law holds up to equivalence: (x+y)*z ≈ x*z + y*z.

Русский

Закон распределения справа сохраняется до эквивалентности: (x+y)*z ≈ x*z + y*z.

LaTeX

$$$(x+y)\cdot z \approx x\cdot z + y\cdot z$$$

Lean4

/-- `(x + y) * z` is equivalent to `x * z + y * z`. -/
theorem right_distrib_equiv (x y z : PGame) : (x + y) * z ≈ x * z + y * z :=
  Quotient.exact <| quot_right_distrib _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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