single_add — Mathlib

English

The operation of taking a single element is additive in its coefficient: single m (r1 + r2) = single m r1 + single m r2.

Русский

Операция создания элементa через coefficient является аддитивной по коэффициенту: single m (r1 + r2) = single m r1 + single m r2.

LaTeX

$$$\\mathrm{single}(m, r_1 + r_2) = \\mathrm{single}(m, r_1) + \\mathrm{single}(m, r_2)$$$

Lean4

@[to_additive]
theorem single_add (m : M) (r₁ r₂ : R) : single m (r₁ + r₂) = single m r₁ + single m r₂ := by simp [single]

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