isIsotypic_iff — Mathlib

English

If there is a linear equivalence e: M ≃ₗ[R] N, IsIsotypic R M is equivalent to IsIsotypic R N.

Русский

Если M линейно эквивалентен N, IsIsotypic R M эквивалентно IsIsotypic R N.

LaTeX

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

Lean4

theorem isIsotypic_iff (e : M ≃ₗ[R] N) : IsIsotypic R M ↔ IsIsotypic R N :=
  ⟨(·.of_injective _ e.symm.injective), (·.of_injective _ e.injective)⟩

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