le_mul_tsub — Mathlib

English

In a distributive ordered ring, for any a,b,c, we have a·b − a·c ≤ a·(b − c).

Русский

В распределимой упорядоченной кольцевой структуре для любых a,b,c выполняется a·b − a·c ≤ a·(b − c).

LaTeX

$$$\forall a,b,c\in R\,(a \cdot b - a \cdot c \le a \cdot (b - c))$$$

Lean4

theorem le_mul_tsub {R : Type*} [Distrib R] [Preorder R] [Sub R] [OrderedSub R] [MulLeftMono R] {a b c : R} :
    a * b - a * c ≤ a * (b - c) :=
  (AddHom.mulLeft a).le_map_tsub (monotone_id.const_mul' a) _ _

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