sndEquiv — Mathlib

English

There is a linear equivalence between Submodule.snd and M₂ given by the second projection.

Русский

Существует линейное эквивалентное отображение между Submodule.snd и M₂ по второй проекции.

LaTeX

$$$\\mathrm{sndEquiv} : \\mathrm{Submodule.snd\\, R\\, M\\, M_2} \\simeq_\\mathsf{R} M_2$$$

Lean4

/-- `N` as a submodule of `M × N` is isomorphic to `N`. -/
@[simps]
def sndEquiv : Submodule.snd R M M₂ ≃ₗ[R] M₂ where
  toFun x := x.1.2
  invFun n := ⟨⟨0, n⟩, by aesop⟩
  map_add' := by simp
  map_smul' := by simp
  left_inv x := by aesop (add norm simp Submodule.snd)

Похожие утверждения