le_isotypicComponent

Mathlib.RingTheory.SimpleModule.Isotypic

URI: https://scilib.ai/kg/mathlib#Submodule.le_isotypicComponent

English

For any linear equivalence e: M ≃ₗ[R] N, IsIsotypic R M ↔ IsIsotypic R N.

Русский

Для линейного эквивалента e между M и N имеем IsIsotypic R M ⇔ IsIsotypic R N.

LaTeX

$$$(e : M \cong_{R} N) \Rightarrow IsIsotypic(R, M) \iff IsIsotypic(R, N)$$$

Lean4

theorem le_isotypicComponent (m : Submodule R M) : m ≤ isotypicComponent R M m :=
  le_sSup ⟨.refl ..⟩

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

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

Разделы

Аффилиация

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