isotypicComponent_eq — Mathlib

English

For any isomorphism e: N ≃ₗ[R] S, the isotypic component of M is the same: isotypicComponent R M N = isotypicComponent R M S.

Русский

При любом изоморфизме e линейном, изотипическая компонента M к N равна той же компоненте к S.

LaTeX

$$$isotypicComponent(R, M, N) = isotypicComponent(R, M, S)$$$

Lean4

theorem isotypicComponent_eq (e : N ≃ₗ[R] S) : isotypicComponent R M N = isotypicComponent R M S :=
  congr_arg sSup <| Set.ext fun _ ↦ Nonempty.congr (·.trans e) (·.trans e.symm)

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