zero_tprodCoeff' — Mathlib

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

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