English
Let X be an object. For any elements r in R(X) and m, m' in A(X), the scalar action distributes over addition in the second argument: r · (m + m') = r · m + r · m'.
Русский
Пусть X — объект. Пусть r ∈ R(X) и m, m' ∈ A(X). Тогда скалярное умножение распределяется по сумме: r · (m + m') = r · m + r · m'.
LaTeX
$$$\forall X\,\forall r\in R(X)\,\forall m,m'\in A(X):\\smul_{\alpha,\varphi}(r, m+m') = smul_{\alpha,\varphi}(r, m) + smul_{\alpha,\varphi}(r, m').$$$
Lean4
protected theorem smul_add : smul α φ r (m + m') = smul α φ r m + smul α φ r m' :=
by
let S := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
have hS : S ∈ J X.unop := by
refine J.intersection_covering (J.intersection_covering ?_ ?_) ?_
all_goals apply Presheaf.imageSieve_mem
apply A.isSeparated _ _ hS
rintro Y f ⟨⟨⟨r₀, hr₀⟩, ⟨m₀ : M₀.obj _, hm₀ : (φ.app _) _ = _⟩⟩, ⟨m₀' : M₀.obj _, hm₀' : (φ.app _) _ = _⟩⟩
rw [(A.val.map f.op).hom.map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀, map_smul_eq α φ r m' f.op r₀ hr₀ m₀' hm₀',
map_smul_eq α φ r (m + m') f.op r₀ hr₀ (m₀ + m₀') (by rw [_root_.map_add, _root_.map_add, hm₀, hm₀']), smul_add,
_root_.map_add]
