isSemisimpleModule_iff_of_bijective

English

If e is a linear isomorphism, then semisimplicity is preserved across the isomorphism.

Русский

Если e — линейное изоморфизм, то полупрямость сохраняется через изоморфизм.

LaTeX

$$IsSemisimpleModule R M ↔ IsSemisimpleModule R N$$

Lean4

theorem _root_.LinearMap.isSemisimpleModule_iff_of_bijective [RingHomSurjective σ] (hl : Function.Bijective l) :
    IsSemisimpleModule R M' ↔ IsSemisimpleModule S N' := by
  simp_rw [isSemisimpleModule_iff, (Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff]
    -- TODO: generalize Submodule.equivMapOfInjective from InvPair to RingHomSurjective

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