English
Let R be a semiring, M an additive commutative monoid equipped with an R-module structure, and M₂ a type with a unique element. Then the product M₂ × M is canonically isomorphic to M via projection to the second factor; i.e., there is a natural linear (R-linear) isomorphism (M₂ × M) ≃_R M obtained by forgetting the first coordinate.
Русский
Пусть R — полукольцо, M — добавочно-коммутативная полугруппа с структурой R-модуля, и M₂ — тип с единственным элементом. Тогда произведение M₂ × M канонически изоморфно M: существует естественное R-линейное изоморождение (M₂ × M) ≃_R M, получающееся по забыванию первого коэффициента.
LaTeX
$$$\\exists \\ell:\\,(M_2 \\times M) \\cong_R M.$$$
Lean4
/-- Multiplying by the trivial module from the left does not change the structure.
This is the `LinearEquiv` version of `AddEquiv.uniqueProd`. -/
@[simps!]
def uniqueProd : (M₂ × M) ≃ₗ[R] M :=
AddEquiv.uniqueProd.toLinearEquiv (by simp [AddEquiv.uniqueProd])
