English
Wedderburn–Artin over algebraically closed fields: a finite-dimensional simple algebra over an algebraically closed field F is isomorphic to a matrix algebra over F.
Русский
Утверждение Ведерберна–Артина над алгебраически замкнутыми полями: простая алгебра конечной размерности над F изоморфна матричной алгебре над F.
LaTeX
$$[IsSimpleRing R] [FiniteDimensional F R] ⇒ ∃ n ≠ 0, Nonempty (R ≃ₐ[F] Matrix(Fin n)(Fin n) F).$$
Lean4
instance instJordanHolderLattice : JordanHolderLattice (Submodule R M)
where
IsMaximal := (· ⋖ ·)
lt_of_isMaximal := CovBy.lt
sup_eq_of_isMaximal hxz hyz := WCovBy.sup_eq hxz.wcovBy hyz.wcovBy
isMaximal_inf_left_of_isMaximal_sup := inf_covBy_of_covBy_sup_of_covBy_sup_left
Iso X Y := Nonempty <| (X.2 ⧸ X.1.comap X.2.subtype) ≃ₗ[R] Y.2 ⧸ Y.1.comap Y.2.subtype
iso_symm := fun ⟨f⟩ => ⟨f.symm⟩
iso_trans := fun ⟨f⟩ ⟨g⟩ => ⟨f.trans g⟩
second_iso {X} {Y}
_ := by
constructor
rw [sup_comm, inf_comm]
dsimp
exact (LinearMap.quotientInfEquivSupQuotient Y X).symm
