finitePresentation_iff — Mathlib

English

For any linear equivalence e, M is finitely presented iff N is finitely presented.

Русский

Для линейного эквивалента e: M ≃ₗ[R] N верно: M FP тогда и только тогда, когда N FP.

LaTeX

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

Lean4

theorem finitePresentation_iff (e : M ≃ₗ[R] N) : Module.FinitePresentation R M ↔ Module.FinitePresentation R N :=
  ⟨fun _ ↦ .of_equiv e, fun _ ↦ .of_equiv e.symm⟩

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