English
The pi construction collects a family of linear maps into a product module, preserving linearity coordinatewise.
Русский
Конструкция pi объединяет семейство линейных отображений в произведение модулей, сохраняя линейность по каждой координате.
LaTeX
$$pi (f) : M2 → (i → φ i)$$
Lean4
/-- `pi` construction for linear functions. From a family of linear functions it produces a linear
function into a family of modules. -/
def pi (f : (i : ι) → M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (i : ι) → φ i :=
{ Pi.addHom fun i => (f i).toAddHom with
toFun := fun c i => f i c
map_smul' := fun _ _ => funext fun i => (f i).map_smul _ _ }
