of_linearEquiv_type

Mathlib.RingTheory.SimpleModule.Isotypic

URI: https://scilib.ai/kg/mathlib#IsIsotypicOfType.of_linearEquiv_type

English

If M is isotypic to S and S is linearly isomorphic to N, then M isotypic to N.

Русский

Если M изотипичен к S и S линейно изоморфен N, то M изотипичен к N.

LaTeX

$$$IsIsotypicOfType(R, M, S) \land (e : S \cong_{R} N) \Rightarrow IsIsotypicOfType(R, M, N)$$$

Lean4

theorem of_linearEquiv_type (h : IsIsotypicOfType R M S) (e : S ≃ₗ[R] N) : IsIsotypicOfType R M N := fun m _ ↦
  ⟨(h m).some.trans e⟩

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

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

Разделы

Аффилиация

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