tsub_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem tsub_mul [MulRightMono R] (a b c : R) : (a - b) * c = a * c - b * c :=
  Contravariant.AddLECancellable.tsub_mul

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