English
Two linear maps φ1, φ2 from the tensor product to E are equal if their compositions with tprod coincide: φ1 ∘ tprod = φ2 ∘ tprod implies φ1 = φ2.
Русский
Два линейных отображения φ1, φ2 из тензорного произведения в E равны, если их композиции с tprod совпадают: φ1 ∘ tprod = φ2 ∘ tprod ⇒ φ1 = φ2.
LaTeX
$$$$ (\phi_1 \circ tprod) = (\phi_2 \circ tprod) \;\Rightarrow\; \phi_1 = \phi_2 $$$$
Lean4
/-- If an element `p` of `FreeAddMonoid (R × Π i, s i)` lifts an element `x` of `⨂[R] i, s i`,
and if `a` is an element of `R`, then the list obtained by multiplying the first entry of each
element of `p` by `a` lifts `a • x`.
-/
theorem lifts_smul {x : ⨂[R] i, s i} {p : FreeAddMonoid (R × Π i, s i)} (h : p ∈ lifts x) (a : R) :
p.map (fun (y : R × Π i, s i) ↦ (a * y.1, y.2)) ∈ lifts (a • x) :=
by
rw [mem_lifts_iff] at h ⊢
rw [← h]
simp [Function.comp_def, mul_smul, List.smul_sum]
