mul_tsub_one — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_tsub_one [AddLeftReflectLE R] (a b : R) : a * (b - 1) = a * b - a := by rw [mul_tsub, mul_one]

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