mul_tsub — 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·b − a·c.

Русский

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

LaTeX

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

Lean4

theorem mul_tsub (a b c : R) : a * (b - c) = a * b - a * c :=
  Contravariant.AddLECancellable.mul_tsub

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