submoduleOfEquivOfLe — Mathlib

English

If p ≤ q, then p viewed as a submodule of q is isomorphic to p via the natural inclusion.

Русский

Если p ≤ q, то p как подмодуль q изоморфен p через естественное вложение.

LaTeX

$$$p \le q \Rightarrow p \text{ как подмодуль } q \cong p$$$

Lean4

/-- If `p ≤ q`, then `p` as a subgroup of `q` is isomorphic to `p`. -/
def submoduleOfEquivOfLe {p q : Submodule R M} (h : p ≤ q) : p.submoduleOf q ≃ₗ[R] p
    where
  toFun m := ⟨m.1, m.2⟩
  invFun m := ⟨⟨m.1, h m.2⟩, m.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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