English
Similarly to the previous item, the map prodUnique : (M × M₂) ≃ₗ[R] M agrees with the classical product-unique isomorphism, i.e., it matches the standard Equiv.prodUnique M M₂.
Русский
Аналогично, линейное эквивалентное сопоставление prodUnique: (M × M₂) ≃ₗ[R] M совпадает с обычной изоморфизмной конструкцией Equiv.prodUnique M M₂.
LaTeX
$$$prodUnique=(R\\!:=R)\\text{ инициализирует привычное }(M\\times M_2)\\cong_R M \\;.$$$
Lean4
/-- Multiplying by the trivial module from the right does not change the structure.
This is the `LinearEquiv` version of `AddEquiv.prodUnique`. -/
@[simps!]
def prodUnique : (M × M₂) ≃ₗ[R] M :=
AddEquiv.prodUnique.toLinearEquiv (by simp [AddEquiv.prodUnique])
