English
For r in R1, z in R, and f in Π i, s i, r • tprodCoeff_R z f = tprodCoeff_R (r • z) f.
Русский
Для любого r ∈ R1, z ∈ R и f ∈ Π i, s_i, выполняется r • tprodCoeff_R z f = tprodCoeff_R (r • z) f.
LaTeX
$$$ r \cdot tprodCoeff(R,z,f) = tprodCoeff(R, r \cdot z, f) $$$
Lean4
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
@[simps]
def prodEquiv [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] :
((M →ₗ[R] M₂) × (M →ₗ[R] M₃)) ≃ₗ[S] M →ₗ[R] M₂ × M₃
where
toFun f := f.1.prod f.2
invFun f := ((fst _ _ _).comp f, (snd _ _ _).comp f)
map_add' _ _ := rfl
map_smul' _ _ := rfl
