simple_of_finrank_eq_one — Mathlib

English

A k-algebra module V of dimension 1 over a field k is simple.

Русский

Модуль V над k размерности 1 является простым.

LaTeX

$$$\dim_k V = 1 \implies \text{Simple}(V)$$$

Lean4

/-- Any `k`-algebra module which is 1-dimensional over `k` is simple. -/
theorem simple_of_finrank_eq_one {k : Type*} [Field k] [Algebra k R] {V : ModuleCat R} (h : finrank k V = 1) :
    Simple V :=
  (simple_iff_isSimpleModule' V).mpr <| (isSimpleModule_iff ..).mpr <| is_simple_module_of_finrank_eq_one h

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