tsub_one_mul — Mathlib

English

Let R be a ring-like ordered additive structure with subtraction. Then for all a,b in R, (a−1)·b = a·b − b.

Русский

Пусть R — кольцообразная упорядоченная аддитивная структура с вычитанием. Тогда для всех a,b ∈ R выполняется (a−1)·b = a·b − b.

LaTeX

$$$(a - 1) \cdot b = a \cdot b - b$$$

Lean4

theorem tsub_one_mul [MulRightMono R] [AddLeftReflectLE R] (a b : R) : (a - 1) * b = a * b - b := by
  rw [tsub_mul, one_mul]

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