map_surjective

Mathlib.RingTheory.Localization.Module

URI: https://scilib.ai/kg/mathlib#LocalizedModule.map_surjective

← MathLib Explorer

English

If l is surjective, then map S l is surjective.

Русский

Если l сюръективно, тогда map S l сюръективно.

LaTeX

$$TODO$$

Lean4

theorem map_surjective (l : M →ₗ[R] N) (hl : Function.Surjective l) : Function.Surjective (map S l) :=
  IsLocalizedModule.map_surjective S (mkLinearMap S M) (mkLinearMap S N) l hl

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

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

Разделы

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

Аффилиация

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