isSimpleModule_iff — Mathlib

English

Let e: M ≃ₗ[R] N. Then M is a simple R-module iff N is a simple R-module.

Русский

Пусть e: M ≃ₗ[R] N. Тогда M прост как модуль над R тогда и только тогда, когда N прост как модуль над R.

LaTeX

$$$\\text{IsSimpleModule } R M \\iff \\text{IsSimpleModule } R N$ при $M \\simeq N$$$

Lean4

theorem isSimpleModule_iff (e : M ≃ₗ[R] N) : IsSimpleModule R M ↔ IsSimpleModule R N :=
  ⟨(·.congr e.symm), (·.congr e)⟩

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