divp_add

Mathlib.Algebra.Ring.Units

URI: https://scilib.ai/kg/mathlib#Units.divp_add

English

Division by a unit distributes over addition as: a /ₚ u + b = (a + b * u) /ₚ u.

Русский

Деление на единицу распределено по сложению: a /ₚ u + b = (a + b * u) /ₚ u.

LaTeX

$$$a /_p u + b = (a + b * u) /_p u$$$

Lean4

theorem divp_add (a b : α) (u : αˣ) : a /ₚ u + b = (a + b * u) /ₚ u := by
  simp only [divp, add_mul, Units.mul_inv_cancel_right]

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

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

Разделы

Аффилиация

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