equiv_comp_of — Mathlib

English

Composing the fgSystem equivalence with the canonical inclusion recovers the canonical subtype map.

Русский

Произведение эквивалентности fgSystem с каноническим вложением восстанавливает каноническое отображение подмодуля как подмодуля.

LaTeX

$$$(\\mathrm{equiv}\\; R\\; M)\\circ \\text{of}_{R,\\iota, G, f} = \\text{N}.1.subtype$$$

Lean4

theorem equiv_comp_of (N : { N : Submodule R M // N.FG }) : (equiv R M).toLinearMap ∘ₗ of _ _ _ _ N = N.1.subtype := by
  ext; simp [equiv]

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