English
An induction principle along a finite index set ι for motives over PiTensorProduct: from the base case 0 and additivity, deduce the property for all elements.
Русский
Принцип индукции по индексу ι для мотива над PiTensorProduct: от базового случая 0 и аддитивности выводим свойство для всех элементов.
LaTeX
$$$\forall z, \text{motive}(z) \;\Leftarrow\; (\text{base case at } 0) \land (\text{closure under } +)$$$
Lean4
/-- `tprodCoeff R r f` with `r : R` and `f : Π i, s i` is the tensor product of the vectors `f i`
over all `i : ι`, multiplied by the coefficient `r`. Note that this is meant as an auxiliary
definition for this file alone, and that one should use `tprod` defined below for most purposes. -/
def tprodCoeff (r : R) (f : Π i, s i) : ⨂[R] i, s i :=
AddCon.mk' _ <| FreeAddMonoid.of (r, f)
