bijective_of_surjective_endomorphism

Mathlib.RingTheory.OrzechProperty

URI: https://scilib.ai/kg/mathlib#OrzechProperty.bijective_of_surjective_endomorphism

English

If f: M → M is surjective, then f is bijective (under the OrzechProperty framework).

Русский

Если f: M → M сюръективно, то f биективно (при условии OrzechProperty).

LaTeX

$$Bijective f when Surjective f.$$

Lean4

theorem bijective_of_surjective_endomorphism (f : M →ₗ[R] M) (hf : Surjective f) : Bijective f :=
  ⟨injective_of_surjective_endomorphism f hf, hf⟩

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

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

Разделы

Аффилиация

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