bot_lt_isotypicComponent — Mathlib

English

If S is simple, then its isotypic component in M is nontrivial: ⊥ < isotypicComponent R M S.

Русский

Если S прост, то его изотипический компонент в M непуст: ⊥ < isotypicComponent R M S.

LaTeX

$$$\bot < isotypicComponent(R, M, S)$$$

Lean4

theorem bot_lt_isotypicComponent (S : Submodule R M) [IsSimpleModule R S] : ⊥ < isotypicComponent R M S :=
  (bot_lt_iff_ne_bot.mpr <| (S.nontrivial_iff_ne_bot).mp <| IsSimpleModule.nontrivial R S).trans_le
    S.le_isotypicComponent

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