English
The equality remains valid when viewed through the Symm embedding; mulMap_left_eq holds at the level of the Symm embedding of Subalgebra.toSubmodule bot.
Русский
Соглашение сохраняется и через симметричное вложение; равенство mulMap_left_eq сохраняется на уровне симметричного вложения Subalgebra.toSubmodule bot.
LaTeX
$$$\\text{RelEmbedding}.instFunLike.coe\\;..\\; mulMap = N.subtype \\circ N.lTensorOne.toLinearMap$$$
Lean4
/-- If `M` is a submodule in an algebra `S` over `R`, there is the natural `R`-linear map
`M ⊗[R] i(R) →ₗ[R] M` induced by multiplication in `S`, here `i : R → S` is the structure map.
This is promoted to an isomorphism of `R`-modules as `Submodule.rTensorOne`. Use that instead. -/
def rTensorOne' : M ⊗[R] (⊥ : Subalgebra R S) →ₗ[R] M :=
show M ⊗[R] Subalgebra.toSubmodule ⊥ →ₗ[R] M from
(LinearEquiv.ofEq _ _ (by rw [Algebra.toSubmodule_bot, mulMap_range, mul_one])).toLinearMap ∘ₗ
(mulMap M _).rangeRestrict
