isNoetherian_of_linearEquiv — Mathlib

English

If f: M ≃ₗ[R] P is a linear equivalence and M is Noetherian, then P is Noetherian.

Русский

Если есть линейное эквивалентное отображение f: M ≃ₗ[R] P и M является Noetherian, то P тоже Noetherian.

LaTeX

$$$\forall f: M \simeq_{\text{lin}} P,\ IsNoetherian R M \Rightarrow IsNoetherian R P$$$

Lean4

theorem isNoetherian_of_linearEquiv (f : M ≃ₗ[R] P) [IsNoetherian R M] : IsNoetherian R P :=
  isNoetherian_of_surjective _ f.toLinearMap f.range

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