sub_divp — Mathlib

English

Let α be a ring, and take elements a, b ∈ α and a unit u ∈ α×. Then a − b /ₚ u = (a · u − b) /ₚ u, i.e. subtracting b divided by a unit is the same as adjusting by the unit.

Русский

Пусть α — кольцо, взять элементы a, b ∈ α и единицу u ∈ α×. Тогда a − b /ₚ u = (a · u − b) /ₚ u, т.е. вычитание b, делённого на единицу, эквивалентно умножению на единицу слева и делению.

LaTeX

$$$a - b^{-1} u = (a u - b) u^{-1}$$$

Lean4

theorem sub_divp (a b : α) (u : αˣ) : a - b /ₚ u = (a * u - b) /ₚ u := by
  simp only [divp, sub_mul, Units.mul_inv_cancel_right]

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