bijective_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 bijective. -/
theorem bijective_of_surjective_endomorphism (f : M →ₗ[R] M) (s : Surjective f) : Bijective f :=
  ⟨IsNoetherian.injective_of_surjective_endomorphism f s, s⟩

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