isIsotypicOfType_iff_type — Mathlib

English

For any linear isomorphism e: N ≃ₗ[R] S, IsIsotypicOfType R M N ↔ IsIsotypicOfType R M S.

Русский

Для линейного изоморфизма e: N ≃ₗ[R] S верно IsIsotypicOfType(R, M, N) ⇔ IsIsotypicOfType(R, M, S).

LaTeX

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

Lean4

theorem isIsotypicOfType_iff_type (e : N ≃ₗ[R] S) : IsIsotypicOfType R M N ↔ IsIsotypicOfType R M S :=
  ⟨(·.of_linearEquiv_type e), (·.of_linearEquiv_type e.symm)⟩

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