of_equiv — Mathlib

English

If e: M ≃ₗ[R] N is a linear equivalence and M is finitely presented, then N is finitely presented.

Русский

Если e: M ≃ₗ[R] N линейное эквивалентность и M FP, то N FP.

LaTeX

$$$(e : M \simeq_{R} N) \Rightarrow (Module.FinitePresentation R M \Rightarrow Module.FinitePresentation R N)$$$

Lean4

theorem of_equiv (e : M ≃ₗ[R] N) [Module.FinitePresentation R M] : Module.FinitePresentation R N := by
  simp [← Module.FinitePresentation.fg_ker_iff e.toLinearMap e.surjective, Submodule.fg_bot]

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