Theorems · Theorem · ring theory

IsSimpleModule.finrank_eq_one_of_isMulCommutative

∀ (A : Type u_1) (V : Type u_2) (k : Type u_3) [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : Module A V] [IsScalarTower k A V] [IsSimpleModule A V]
  [FiniteDimensional k V] [IsAlgClosed k] [IsMulCommutative A], Module.finrank k V = 1

Any finite-dimensional irreducible representation of a commutative algebra over an algebraically closed field is one-dimensional.

Defined in

Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Cited by

1 results in Mathlib

Foundations

Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingAlgebraAddCommGroupModuleModuleIsScalarTowerIsSimpleModuleFiniteDimensionalIsAlgClosedIsMulCommutative