injective_of_surjective_endomorphism

English

Any surjective endomorphism of a Noetherian module is bijective.

Русский

Любой сюръективный эндоморфизм Нётерова модуля биективен.

LaTeX

$$$\\text{If } f: M \\to M \\text{ is surjective and } M \\text{ is Noetherian}, \\text{ then } f \\text{ is bijective}$$$

Lean4

/-- Any surjective endomorphism of a Noetherian module is injective. -/
theorem injective_of_surjective_endomorphism (f : M →ₗ[R] M) (s : Surjective f) : Injective f :=
  IsNoetherian.injective_of_surjective_of_injective _ f (LinearEquiv.refl _ _).injective s

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