fg_of_linearEquiv — Mathlib

English

If a property P holds for spans of single elements and is preserved under finite joins, then P holds for every finitely generated submodule.

Русский

Если P верно для порождений по одному элементу и сохраняется при конечном объединении, то P верно для любого FG-подмодуля.

LaTeX

$$⟨∀ x, P( span R {x} ), ∀ M1 M2, P M1 → P M2 → P (M1 ⊔ M2)⟩ ∧ N.FG → P N$$

Lean4

theorem fg_of_linearEquiv (e : M ≃ₗ[R] P) (h : (⊤ : Submodule R P).FG) : (⊤ : Submodule R M).FG :=
  e.symm.range ▸ map_top (e.symm : P →ₗ[R] M) ▸ h.map _

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