add_divp

Mathlib.Algebra.Ring.Units

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

English

Addition interacts with division by a unit as: a + (b /ₚ u) = (a u + b) /ₚ u.

Русский

Сложение и деление на единицу взаимодействуют так: a + (b /ₚ u) = (a u + b) /ₚ u.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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