English
Construct an additive homomorphism from a universal construction (PiTensorProduct) to F, given a function φ with suitable coherence conditions (C0, C0', C_add, C_add_scalar, C_smul).
Русский
Построение аддитивного однородного отображения (AddMonoidHom) из универсального конструирования (PiTensorProduct) в F, заданного функцией φ при условии согласованности (C0, C0', C_add, C_add_scalar, C_smul).
LaTeX
$$$\mathrm{liftAddHom}(\phi, C_0, C_0', C_{add}, C_{add\_scalar}, C_{smul}) : (\bigotimes_R s_i ) \to_+ F$$$
Lean4
theorem zero_tprodCoeff' (z : R) (f : Π i, s i) (i : ι) (hf : f i = 0) : tprodCoeff R z f = 0 :=
Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero _ _ i hf