divp_sub

Mathlib.Algebra.Ring.Units

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

← MathLib Explorer

English

Let α be a ring, and a, b ∈ α with u ∈ α×. Then a /ₚ u − b = (a − b · u) /ₚ u.

Русский

Пусть α — кольцо, a, b ∈ α и u ∈ α×. Тогда a /ₚ u − b = (a − b · u) /ₚ u.

LaTeX

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

Lean4

theorem divp_sub (a b : α) (u : αˣ) : a /ₚ u - b = (a - b * u) /ₚ u :=
  by
  simp only [divp, sub_mul, sub_right_inj]
  rw [mul_assoc, Units.mul_inv, mul_one]

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

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

Разделы

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

Аффилиация

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