isNoetherian_of_injective

Mathlib.RingTheory.Noetherian.Basic

URI: https://scilib.ai/kg/mathlib#isNoetherian_of_injective

← MathLib Explorer

English

If P is Noetherian and f: M →ₗ[R] P is injective, then M is Noetherian.

Русский

Если P — Noetherian, а f: M →ₗ[R] P инъективно, то M — Noetherian.

LaTeX

$$$[IsNoetherian R P]\to (\text{Injective } f) \Rightarrow IsNoetherian R M$$$

Lean4

theorem isNoetherian_of_injective [IsNoetherian R P] (f : M →ₗ[R] P) (hf : Function.Injective f) : IsNoetherian R M :=
  isNoetherian_of_linearEquiv (LinearEquiv.ofInjective f hf).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru