congr

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#IsSimpleModule.congr

English

If e: M ≃ₗ[R] N and N is a simple R-module, then M is a simple R-module as well.

Русский

Если e: M ≃ₗ[R] N и N — простой R-модуль, то и M — простой R-модуль.

LaTeX

$$$\\text{IsSimpleModule } R N \\;\\rightarrow\\; \\text{IsSimpleModule } R M$ (via $e$)$$

Lean4

theorem congr (e : M ≃ₗ[R] N) [IsSimpleModule R N] : IsSimpleModule R M where
  __ := (Submodule.orderIsoMapComap e).isSimpleOrder

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

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

Разделы

Аффилиация

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