divp_add_divp_same

Mathlib.Algebra.Ring.Units

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

English

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

Русский

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

LaTeX

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

Lean4

theorem divp_add_divp_same (a b : α) (u : αˣ) : a /ₚ u + b /ₚ u = (a + b) /ₚ u := by simp only [divp, add_mul]

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

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

Разделы

Аффилиация

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