fstEquiv — Mathlib

English

The proof that fstEquiv is a linear equivalence between Submodule.fst and M.

Русский

Доказательство того, что fstEquiv является линейным эквивалентом между Submodule.fst и M.

LaTeX

$$$\\text{fstEquiv} : \\mathrm{Submodule.fst\\, R\\, M\\, M_2} \\simeq_\\mathsf{R} M$$$

Lean4

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

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